proposition: Lemma fldmultinvlax' {X: fld} (e : X) (ne : e != 0%ring) : (fldmultinv' e * e)%ring = 1%ring.
proof: Proof. unfold fldmultinv'. destruct (fldchoice0 _). - contradiction. - apply fldmultinvlax. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings