proposition: Lemma CReal_opp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2.
proof: Proof. intros. apply (CReal_plus_eq_reg_l (r1+r2)). rewrite CReal_plus_opp_r, (CReal_plus_comm (-r1)), CReal_plus_assoc. rewrite <- (CReal_plus_assoc r2), CReal_plus_opp_r, CReal_plus_0_l. rewrite CReal_plus_opp_r. reflexivity. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra