proposition: Lemma Ropp_eq_reg : forall r1 r2, - r1 = - r2 -> r1 = r2.
proof: Proof. intros r1 r2 H; rewrite <-(Ropp_involutive r1), <-(Ropp_involutive r2). now apply Ropp_eq_compat. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField