Lemma hzeqbooleqii (i : hz) : hzbooleq i i = true. Proof. unfold hzbooleq. unfold decreltobrel. induction (pr2 hzdeceq i i) as [T | F]. - apply idpath. - apply fromempty. apply F. apply idpath. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.