proposition: Lemma CReal_opp_0 : -0 == 0.
proof: Proof. apply (CReal_plus_eq_reg_l 0). rewrite CReal_plus_0_r, CReal_plus_opp_r. reflexivity. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra