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