proposition: Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 = 0 -> r2 = - r1.
proof: Proof. intros r1 r2 H%(Rplus_eq_compat_l (- r1)). now rewrite <-Rplus_assoc, Rplus_opp_l, Rplus_0_l, Rplus_0_r in H. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField