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