proposition: Lemma Rplus_minus_r : forall r1 r2, r1 + r2 - r2 = r1.
proof: Proof. now intros r1 r2; unfold Rminus; rewrite Rplus_assoc, Rplus_opp_r, Rplus_0_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField