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