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