proposition: Lemma RState_Trans : forall s1 s2 s3 : S, RState s1 s2 -> RState s2 s3 -> RState s1 s3.
proof: Proof. simple induction 2; intros. assumption. apply rsNextTick; trivial. apply (rsNextDisc H2 H3 H4). Qed.
imports: time_clocks