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