Definition hzabsvalnat n : hzabsval (natnattohz n 0) = n. Proof. intros. unfold hzabsval. unfold setquotuniv. simpl. unfold hzabsvalint. simpl. destruct (natgthorleh n 0). { apply natminuseqn. } { exact (! (natleh0tois0 h)). } Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.