proposition: Lemma CReal_opp_mult_distr_r : forall r1 r2 : CReal, - (r1 * r2) == r1 * (- r2).
proof: Proof. intros. apply (CReal_plus_eq_reg_l (r1*r2)). rewrite CReal_plus_opp_r, <- CReal_mult_plus_distr_l. symmetry. apply CReal_mult_proper_0_l. apply CReal_plus_opp_r. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra