proposition: Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 = 0 -> r1 = r2.
proof: Proof. unfold Rminus; intros r1 r2 H%(Rplus_eq_compat_r r2). now rewrite Rplus_assoc, Rplus_opp_l, Rplus_0_l, Rplus_0_r in H. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField