proposition: Lemma Rlt_transitive : Ctransitive Rlt.
proof: Proof. intros x y z H H'. simpl in H, H'. elim H; intros N1 HN1; elim HN1; clear H HN1; intros e1 He1 HN1. elim H'; intros N2 HN2; elim HN2; clear H' HN2; intros e2 He2 HN2. exists (Nat.max N1 N2); exists (e1[+]e2). apply plus_resp_pos; auto. intros; rstepr (CS_seq _ y n[-]CS_seq _ x n[+] (CS_seq _ z n[-]CS_seq _ y n)). apply plus_resp_leEq_both; eauto with arith. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection