proposition: Lemma MAX_strext : bin_op_strext _ MAX.
proof: Proof. unfold bin_op_strext in |- *. unfold bin_fun_strext in |- *. intros x1 x2 y1 y2 H. generalize (ap_imp_less _ _ _ H); intro H0. elim H0; intro H1. generalize (less_MAX_imp _ _ _ H1); intro H2. elim H2; intro H3. left. apply less_imp_ap. apply leEq_less_trans with (MAX x1 y1); auto. apply lft_leEq_MAX. right. apply less_imp_ap. apply leEq_less_trans with (MAX x1 y1); auto. apply rht_leEq_MAX. generalize (less_MAX_imp _ _ _ H1); intro H2. elim H2; intro. left. apply Greater_imp_ap. apply leEq_less_trans with (MAX x2 y2); auto. apply lft_leEq_MAX. right. apply Greater_imp_ap. apply leEq_less_trans with (MAX x2 y2); auto. apply rht_leEq_MAX. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq