proposition: Lemma Rdiv_mult_r_l : forall r r1 r2, r <> 0 -> (r1 * r) / (r * r2) = r1 / r2.
proof: Proof. now intros r r1 r2; rewrite (Rmult_comm r1); apply Rdiv_mult_l_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField