Definition isnonzerorig (X : rig) : hProp. Proof. intros; use make_hProp. - exact ((1 : X) != 0). - apply isapropneg. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.