Lemma hzeqeisi {i i0 : hz} (e : hzeq i i0) (e' : hzeq i (i0 + 1)) : empty. Proof. apply nopathstruetofalse. use (pathscomp0 _ (hzbooleqisi i0)). rewrite <- e'. rewrite <- e. apply (! (hzeqbooleqii i)). Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.