Lemma fldmultinvlax' {X: fld} (e : X) (ne : e != 0%ring) : (fldmultinv' e * e)%ring = 1%ring. Proof. unfold fldmultinv'. destruct (fldchoice0 _). - contradiction. - apply fldmultinvlax. 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.