proposition: Lemma part_function_Max_strext : forall x y (Hx : Conj P Q x) (Hy : Conj P Q y), Max (F x (Prj1 Hx)) (G x (Prj2 Hx)) [#] Max (F y (Prj1 Hy)) (G y (Prj2 Hy)) -> x [#] y.
proof: Proof. intros. rename X into H. elim (cs_bin_op_strext _ _ _ _ _ _ H). exact (pfstrx _ F _ _ _ _). exact (pfstrx _ G _ _ _ _). Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq