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