proposition: Lemma Max_less : forall x y z : IR, x [<] z -> y [<] z -> Max x y [<] z.
proof: Proof. intros. elim (smaller _ (z[-]x) (z[-]y)). intro e. intros H1 H2. elim H2. clear H2. intros H2 H3. cut (z[-]e [/]TwoNZ [<] z). intro H4. elim (less_cotransitive_unfolded _ _ _ H4 (Max x y)); intros H5. elim (less_Max_imp _ _ _ H5); intros H6. cut (Not (e [/]TwoNZ [<] z[-]x)). intro H7. elim H7. apply less_leEq_trans with e; auto. apply pos_div_two'; auto. apply less_antisymmetric_unfolded. apply shift_minus_less. apply shift_less_plus'. auto. cut (Not (e [/]TwoNZ [<] z[-]y)). intro H7. elim H7. apply less_leEq_trans with e; auto. apply pos_div_two'; auto. apply less_antisymmetric_unfolded. apply shift_minus_less. apply shift_less_plus'. auto. auto. apply shift_minus_less. astepl (z[+][0]). apply plus_resp_less_lft. apply pos_div_two. auto. apply shift_less_minus. astepl x. auto. apply shift_less_minus. astepl y. auto. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq