proposition: Lemma equal_dec_quotients (a b c d : F) : b ≠ 0 → d ≠ 0 → (a * d = c * b ↔ a / b = c / d).
proof: Proof. Proof with trivial; try ring. split; intro E. apply (right_cancellation_ne_0 (.*.) b)... apply (right_cancellation_ne_0 (.*.) d)... transitivity (a * d * (b * /b))... transitivity (c * b * (d * /d))... rewrite E, dec_recip_inverse, dec_recip_inverse... transitivity (a * d * 1)... rewrite <-(dec_recip_inverse b)... transitivity (a * / b * d * b)... rewrite E. transitivity (c * (d * / d) * b)... rewrite dec_recip_inverse... 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