proposition: Lemma CRealLt_proper_l : forall x y z : CReal, CRealEq x y -> CRealLt x z -> CRealLt y z.
proof: Proof. intros x y z Hxeqy Hxltz. apply (CRealLt_morph x y Hxeqy z z). - apply CRealEq_refl. - apply Hxltz. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra