proposition: Lemma Rdiv_mult_distr : forall r1 r2 r3, r1 / (r2 * r3) = r1 / r2 / r3.
proof: Proof. now unfold Rdiv; intros r1 r2 r3; rewrite Rinv_mult, Rmult_assoc. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField