proposition: Theorem rdiv4 a b c d : ~ b == 0 -> ~ d == 0 -> (a / b) * (c / d) == (a * c) / (b * d).
proof: Proof. intros H H0. assert (~ b * d == 0) by now apply field_is_integral_domain. apply rmul_reg_l with (b * d); trivial. rewrite rdiv_simpl; trivial. transitivity (b * (a / b) * (d * (c / d))); [ ring | ]. rewrite !rdiv_simpl; trivial. Qed.
imports: ZArith_base