proposition: Lemma CReal_plus_proper_l : forall x y z : CReal, CRealEq x y -> CRealEq (CReal_plus z x) (CReal_plus z y).
proof: Proof. intros. split. - intro abs. apply CReal_plus_lt_reg_l in abs. destruct H. contradiction. - intro abs. apply CReal_plus_lt_reg_l in abs. destruct H. contradiction. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra