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