proposition: Lemma Rdiv_diag_uniq : forall r1 r2, r1 / r2 = 1 -> r1 = r2.
proof: Proof. intros r1 r2; destruct (Req_dec r2 0) as [-> | Hn0]. - now intros H; rewrite Rdiv_0_r in H; exfalso; apply R1_neq_R0; symmetry. - intros H%(Rmult_eq_compat_r r2). now rewrite <-Rmult_div_swap, Rmult_div_l, Rmult_1_l in H. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField