proposition: Theorem rdiv4b a b c d e f : ~ b * e == 0 -> ~ d * f == 0 -> ((a * f) / (b * e)) * ((c * e) / (d * f)) == (a * c) / (b * d).
proof: Proof. intros H H0. assert (~ b == 0) by (contradict H; rewrite H; ring). assert (~ e == 0) by (contradict H; rewrite H; ring). assert (~ d == 0) by (contradict H0; rewrite H0; ring). assert (~ f == 0) by (contradict H0; rewrite H0; ring). assert (~ b*d == 0) by now apply field_is_integral_domain. assert (~ e*f == 0) by now apply field_is_integral_domain. rewrite rdiv4; trivial. transitivity ((e * f) * (a * c) / ((e * f) * (b * d))). - apply rdiv_ext; ring. - rewrite <- rdiv4, rdiv_r_r; trivial. Qed.
imports: ZArith_base