proposition: Lemma dec_quotients (a c b d : F) : b ≠ 0 → d ≠ 0 → a / b + c / d = (a * d + c * b) / (b * d).
proof: Proof. Proof with auto. intros A B. assert (a / b = (a * d) / (b * d)) as E1. apply ->equal_dec_quotients... ring. intros G. destruct (zero_product b d)... assert (c / d = (b * c) / (b * d)) as E2. apply ->equal_dec_quotients... ring. intros G. destruct (zero_product b d)... rewrite E1, E2. ring. Qed.
imports: Coq.setoid_ring.Field Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.fields MathClasses.theory.strong_setoids MathClasses.theory.rings