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