proposition: Lemma Rdiv_eq_reg_r : forall r r1 r2, r1 / r = r2 / r -> r <> 0 -> r1 = r2.
proof: Proof. now unfold Rdiv; intros r r1 r2 H H'%Rinv_neq_0_compat; apply (Rmult_eq_reg_r (/ r)). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField