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