proposition: Lemma Rminus_plus_r_r : forall r r1 r2, (r1 + r) - (r2 + r) = r1 - r2.
proof: Proof. intros r r1 r2; rewrite Rminus_plus_distr, Rplus_comm. now rewrite <-Rplus_minus_assoc, Rplus_minus_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField