proposition: Theorem rdiv2b a b c d e : ~ (b*e) == 0 -> ~ (d*e) == 0 -> a / (b*e) + c / (d*e) == (a * d + c * b) / (b * (d * e)).
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 (~ b * (d * e) == 0) by (repeat apply field_is_integral_domain; trivial). apply rmul_reg_l with (b * (d * e)); trivial. rewrite rdiv_simpl; trivial. rewrite rdistr_r. apply radd_ext. - transitivity ((b * e) * (a / (b * e)) * d); [ ring | now rewrite rdiv_simpl ]. - transitivity ((d * e) * (c / (d * e)) * b); [ ring | now rewrite rdiv_simpl ]. Qed.
imports: ZArith_base