Definition fldmultinvpair (X : fld) (x : X) (ne : x != 0) : multinvpair X x. Proof. intros. induction (fldchoice x) as [ ne0 | e0 ]. - apply ne0. - induction (ne e0). Defined.
Require Import UniMath.Algebra.Groups.