Definition hz_to_normal_form (i:ℤ) : hz_normal_form i. Proof. intros. destruct (hzlthorgeh i 0) as [r|s]. { apply inr. assert (a := hzabsvallth0 r). assert (b := hzlthtoneq _ _ r). assert (c := hzabsvalneq0 b). assert (d := natneq0togth0 _ c). assert (f := natgthtogehsn _ _ d). assert (g := minusplusnmm _ _ f). rewrite natpluscomm in g. simpl in g. exists (hzabsval i - 1)%nat. rewrite g. apply hzinvmaponpathsminus. exact a. } { apply inl. exists (hzabsval i). exact (hzabsvalgeh0 s). } Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.