proposition: Lemma Rminus_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 - r = r2 - r.
proof: Proof. now unfold Rminus; intros r r1 r2;apply Rplus_eq_compat_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField