proposition: Theorem rdiv2 a b c d : ~ b == 0 -> ~ d == 0 -> a / b + c / d == (a * d + c * b) / (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. rewrite rdistr_r. apply radd_ext. - now rewrite <- rmul_assoc, (rmul_comm d), rmul_assoc, rdiv_simpl. - now rewrite (rmul_comm c), <- rmul_assoc, rdiv_simpl. Qed.
imports: ZArith_base