(x y : F) : x / y = 1 -> x = y. 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.
Require Import