proposition: Lemma Rmult_inv_r_uniq : forall r1 r2, r1 <> 0 -> r1 * r2 = 1 -> r2 = / r1.
proof: Proof. intros r1 r2 Hn0 H%(Rmult_eq_compat_l (/ r1)). now rewrite <-Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_1_l in H. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField