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