proposition: Lemma CReal_plus_opp_l : forall x : CReal, - x + x == 0.
proof: Proof. intro x. rewrite CReal_plus_comm. apply CReal_plus_opp_r. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra