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