proposition: Lemma CReal_plus_proper_r : forall x y z : CReal, CRealEq x y -> CRealEq (CReal_plus x z) (CReal_plus y z).
proof: Proof. intros. apply (CRealEq_trans _ (CReal_plus z x)). - apply CReal_plus_comm. - apply (CRealEq_trans _ (CReal_plus z y)). 2: apply CReal_plus_comm. 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