proposition: Lemma R_plus_resp_lt : forall x y, Rlt x y -> forall z, Rlt (x[+]z) (y[+]z).
proof: Proof. intros x y Hxy z. elim Hxy; intros N HN; elim HN; clear Hxy HN; intros e He HN; exists N; exists e; auto; intros n Hn. simpl in |- *; rstepr (CS_seq _ y n[-]CS_seq _ x n); auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection