proposition: Lemma Rdiv_mult_r_r : forall r r1 r2, r <> 0 -> (r1 * r) / (r2 * r) = r1 / r2.
proof: Proof. intros r r1 r2 H. rewrite <-Rmult_div_assoc, (Rmult_comm r2), Rdiv_mult_distr. now rewrite Rdiv_diag by exact H; rewrite Rdiv_1_l, Rdiv_def. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField