proposition: Lemma Rinv_mult_distr_depr : forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2.
proof: Proof. now intros r1 r2 _ _; apply Rinv_mult. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField