Move "classic" Prosa to rt.classic namespace and update documentation

As a first step towards completing #53 (closed) and #54 (closed), this MR moves the "old" Prosa to the rt.classic namespace and updates the documentation to reflect the "modern" Prosa.

restructuring/analysis/basic_facts/service.v

@@ -164,8 +164,8 @@ Section UnitService.
   Proof.
     unfold service_during; intros t delta.
     apply leq_trans with (n := \sum_(t <= t0 < t + delta) 1);
-      last by simpl_sum_const; rewrite addKn leqnn.
-      by apply: leq_sum => t' _; apply: service_at_most_one.
+      last by rewrite sum_of_ones.
+    by apply: leq_sum => t' _; apply: service_at_most_one.
   Qed.
 
   Section ServiceIsAStepFunction.