Definition fldfracmultinvint (X : intdom) (is : isdeceq X) (xa : X × intdomnonzerosubmonoid X) : X × intdomnonzerosubmonoid X. Proof. intros. induction (is (pr1 xa) 0) as [ e0 | ne0 ]. - apply (1 ,, (1 ,, nonzeroax X)). - apply (pr12 xa ,, pr1 xa ,, ne0). Defined.
Require Import UniMath.Algebra.Groups.