proposition: Lemma leEq_distr_AbsIR : forall x y : IR, [0] [<] x -> x [<=] AbsIR y -> {x [<=] y} + {y [<=] [--]x}.
proof: Proof. intros. cut (x[*]Three [/]FourNZ [<] AbsIR y); intros. elim (less_AbsIR (x[*]Three [/]FourNZ) y); intros; [ left | right | idtac | auto ]. astepr ([0][+]y); apply shift_leEq_plus. apply approach_zero. cut (forall e : IR, [0] [<] e -> e [<] x [/]TwoNZ -> x[-]y [<] e); intros. cut (x [/]FourNZ [<] x [/]TwoNZ); intros. 2: rstepl ((x [/]TwoNZ) [/]TwoNZ); apply pos_div_two'; apply pos_div_two; auto. rename X3 into H4. elim (less_cotransitive_unfolded _ _ _ H4 e); intro. apply leEq_less_trans with (x [/]FourNZ); auto. apply less_leEq. apply shift_minus_less; apply shift_less_plus'. rstepl (x[*]Three [/]FourNZ); auto. rename X1 into H2. apply H2; auto. apply shift_minus_less; apply shift_less_plus'. cut (x[-]e [<] AbsIR y); intros. 2: apply less_leEq_trans with x; auto. 2: apply shift_minus_less; apply shift_less_plus'; astepl ZeroR; auto. elim (less_AbsIR (x[-]e) y); auto. intro; exfalso. apply (less_irreflexive_unfolded _ y). eapply leEq_less_trans. 2: apply a. apply less_leEq; eapply less_transitive_unfolded. apply b. astepl ([0][-] (x[-]e)). apply shift_minus_less. astepr (x[*]Three [/]FourNZ[+]x[-]e). apply shift_less_minus; astepl e. eapply less_leEq_trans. rename X2 into H3. apply H3. apply less_leEq. rstepl (x[*] ([0][+][0][+][1] [/]TwoNZ)); rstepr (x[*] ([1][+][1] [/]FourNZ[+][1] [/]TwoNZ)). apply mult_resp_less_lft; auto. apply plus_resp_less_rht; apply plus_resp_less_leEq. apply pos_one. apply less_leEq; apply pos_div_four; apply pos_one. apply shift_less_minus; astepl e. eapply less_leEq_trans. rename X2 into H3. apply H3. apply less_leEq; apply pos_div_two'; auto. astepr ([0][+][--]x); apply shift_leEq_plus. apply leEq_wdl with (y[+]x). 2: unfold cg_minus in |- *; algebra. apply approach_zero. cut (forall e : IR, [0] [<] e -> e [<] x [/]TwoNZ -> y[+]x [<] e); intros. cut (x [/]FourNZ [<] x [/]TwoNZ); intros. 2: rstepl ((x [/]TwoNZ) [/]TwoNZ); apply pos_div_two'; apply pos_div_two; auto. rename X3 into H4. elim (less_cotransitive_unfolded _ _ _ H4 e); intro. apply leEq_less_trans with (x [/]FourNZ); auto. apply less_leEq; apply shift_plus_less. rstepr ( [--] (x[*]Three [/]FourNZ)); auto. rename X1 into H2. apply H2; auto. cut (x[-]e [<] AbsIR y); intros. 2: apply less_leEq_trans with x; auto. 2: apply shift_minus_less; apply shift_less_plus'; astepl ZeroR; auto. elim (less_AbsIR (x[-]e) y); auto. intro; exfalso. apply (less_irreflexive_unfolded _ y). eapply leEq_less_trans. 2: apply a. apply less_leEq; eapply less_transitive_unfolded. apply b. apply shift_less_minus; apply shift_plus_less'. eapply less_transitive_unfolded. rename X2 into H3. apply H3. rstepl (x[*] ([0][+][0][+][1] [/]TwoNZ)); rstepr (x[*] ([1][+][1] [/]FourNZ[+][1] [/]TwoNZ)). apply mult_resp_less_lft; auto. apply plus_resp_less_rht; apply plus_resp_less_leEq. apply pos_one. apply less_leEq; apply pos_div_four; apply pos_one. intro. rstepl (y[-][--]x). apply shift_minus_less. rstepr ( [--] (x[-]e)); auto. apply shift_less_minus; astepl e. eapply less_leEq_trans. rename X2 into H3. apply H3. apply less_leEq; apply pos_div_two'; auto. astepl (ZeroR[*]Three [/]FourNZ). apply mult_resp_less; auto. apply pos_div_four; apply pos_three. apply less_leEq_trans with x; auto. astepr (x[*][1]). astepr (x[*]Four [/]FourNZ). apply mult_resp_less_lft; auto. apply div_resp_less. apply pos_four. apply three_less_four. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq