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

 From mathcomp Require Import ssrnat ssrbool fintype.
+
 From rt.restructuring.behavior Require Export all.
 From rt.restructuring.model.processor Require Export platform_properties.
 From rt.util Require Import tactics step_function sum.
@@ -163,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.
@@ -289,7 +290,8 @@ Section RelationToScheduled.
       case (boolP([exists t: 'I_t2,
                       (t >= t1) && (service_at sched j t > 0)])) => [EX | ALL].
       - move: EX => /existsP [x /andP [GE SERV]].
-        exists x; split; auto.
+        exists x; split => //.
+        apply /andP; by split.
       - rewrite negb_exists in ALL; move: ALL => /forallP ALL.
         rewrite /service_during big_nat_cond in NONZERO.
         rewrite big1 ?ltn0 // in NONZERO => i.