(a c b d : F) : b <> 0 -> d <> 0 -> a / b + c / d = (a * d + c * b) / (b * d). Proof. intros A B. assert (a / b = (a * d) / (b * d)) as E1. - apply equal_dec_quotients;auto. + solve_propholds. + rewrite (mult_comm b);apply associativity. - assert (c / d = (b * c) / (b * d)) as E2. + apply equal_dec_quotients;trivial. * solve_propholds. * rewrite mult_assoc, (mult_comm c). reflexivity. + rewrite E1, E2. rewrite (mult_comm c b). apply symmetry, simple_distribute_r. Qed.
Require Import