Lemma hzbooleqisi' (i : hz) : hzbooleq i (i + 1) = false. Proof. apply negrtopaths. apply (negf (λ e, hzpluslcan _ _ _ (! (hzplusr0 i @ e)))); clear i. simple refine (confirm_not_equal isdecrelhzeq _ _ _). reflexivity. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.