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