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