proposition: Lemma CReal_opp_involutive : forall x:CReal, --x == x.
proof: Proof. intros. apply (CReal_plus_eq_reg_l (-x)). rewrite CReal_plus_opp_l, CReal_plus_opp_r. reflexivity. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra