Lemma nattorig_nattohz : ∏ n : nat, nattorig (X := hz) n = nattohz n. Proof. induction n as [|n IHn]. - unfold nattorig, nattohz ; simpl. reflexivity. - rewrite nattorigS, IHn. apply pathsinv0, nattohzandS. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.