proposition: Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) = - r1 + - r2.
proof: Proof. intros r1 r2; symmetry. apply Rplus_opp_r_uniq. rewrite (Rplus_comm r1), Rplus_assoc, <-(Rplus_assoc r1), Rplus_opp_r. now rewrite Rplus_0_l, Rplus_opp_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField