proposition: Lemma Rlt_alt_2 : forall x y : R_Set, Rlt x y -> {e : F | [0] [<] e | {N : nat | forall m, N <= m -> e [<=] CS_seq F y m[-]CS_seq F x m}}.
proof: Proof. intros x y H. unfold Rlt in H. case H. intros N H2. case H2. intros e H1 H0. exists e. assumption. exists N. auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection