proposition: Lemma equal_by_one_quotient (x y : F) : x / y = 1 → x = y.
proof: Proof. intro Exy. destruct (decide (y = 0)) as [Ey|Ey]. exfalso. apply (is_ne_0 1). rewrite <- Exy, Ey, dec_recip_0. ring. apply (right_cancellation_ne_0 (.*.) (/y)). now apply dec_recip_ne_0. now 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