Lemma hzeqissi {i : hz} (e : hzeq i (i + 1 + 1)) : empty. Proof. set (tmp := hzbooleqissi i). cbn in e. rewrite <- e in tmp. rewrite (hzeqbooleqii i) in tmp. apply nopathstruetofalse. apply tmp. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.