proposition: Lemma fldmultinvrax {X: fld} (e : X) (ne : e != 0%ring) : (e * fldmultinv e ne)%ring = 1%ring.
proof: Proof. exact (pr2 (pr2 (fldmultinvpair _ e ne))). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings