proposition: Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) = r2 - r1.
proof: Proof. unfold Rminus; intros r1 r2. now rewrite Ropp_plus_distr, Ropp_involutive, Rplus_comm. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField