Definition fldmultinv' {X : fld} (e : X) : X. Proof. destruct (fldchoice0 e) as [eq0 | neq]. - exact 0%ring. - exact (fldmultinv e neq). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.RigsAndRings.