proposition: Lemma quotients (a c : F) (b d : F ₀) : a // b + c // d = (a * `d + c * `b) // (b * d).
proof: Proof. setoid_replace (a // b) with ((a * `d) // (b * d)) by (apply equal_quotients; simpl; ring). setoid_replace (c // d) with ((`b * c) // (b * d)) by (apply equal_quotients; simpl; ring). ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.fields