proposition: Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r = r2 + r -> r1 = r2.
proof: Proof. intros r r1 r2 H; rewrite 2(Rplus_comm _ r) in H. now apply (Rplus_eq_reg_l r). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField