proposition: Lemma equal_quotients (a c: F) b d : a * `d = c * `b ↔ a // b = c // d.
proof: Proof. Proof with try ring. split; intro E. transitivity (1 * (a // b))... rewrite <- (recip_inverse d). transitivity (// d * (a * `d) // b)... rewrite E. transitivity (// d * c * (`b // b))... rewrite recip_inverse... transitivity (a * `d * 1)... rewrite <- (recip_inverse b). transitivity (a // b * `d * `b)... rewrite E. transitivity (c * (`d // d) * `b)... rewrite recip_inverse... Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids MathClasses.theory.rings