proposition: Lemma CRlt_max : forall {R : ConstructiveReals} (x y z : CRcarrier R), CRmax x y < z -> prod (x < z) (y < z).
proof: Proof. intros. destruct (CR_Q_dense R _ _ H) as [q qmaj]. destruct qmaj. split. - apply (CRlt_le_trans _ (CR_of_Q R q)). + apply (CRle_lt_trans _ (CRmax x y)). * apply CRmax_l. * exact c. + apply CRlt_asym, c0. - apply (CRlt_le_trans _ (CR_of_Q R q)). + apply (CRle_lt_trans _ (CRmax x y)). * apply CRmax_r. * exact c. + apply CRlt_asym, c0. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms