proposition: Lemma Rlt_alt_1 : forall x y : R_Set, {e : F | [0] [<] e | {N : nat | forall m, N <= m -> e [<=] CS_seq F y m[-]CS_seq F x m}} -> Rlt x y.
proof: Proof. intros x y H. case H. intro e1. intros H1 H2. case H2. intro N1. intros H3. unfold Rlt in |- *. exists N1. exists (e1 [/]TwoNZ). apply pos_div_two. assumption. intros. apply leEq_transitive with e1. apply mult_cancel_leEq with (Two:F). apply pos_two. rstepl (e1[+] ([0]:F)). rstepr (e1[+]e1). apply plus_resp_leEq_lft. apply less_leEq; assumption. apply H3. assumption. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection