proposition: Lemma equal_by_one_quotient (x y : F) : x / y = 1 -> x = y.
proof: Proof. intro Exy. destruct (dec (y = 0)) as [Ey|Ey]. - destruct (is_ne_0 1). rewrite <- Exy, Ey, dec_recip_0. apply mult_0_r. - apply (right_cancellation_ne_0 (.*.) (/y)). + apply dec_recip_ne_0. trivial. + rewrite dec_recip_inverse;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.fields HoTT.Classes.theory.apartness HoTT.Classes.theory.rings