Lemma isdecrelhzeqpii (i : hz) : isdecrelhzeq (i - 1) i = ii2 (fun (e : hzeq (i - 1) i) => hzeqpii e). Proof. induction (isdecrelhzeq (i - 1) i) as [e | n]. - apply fromempty. apply (hzeqpii e). - apply maponpaths. apply funextfun. intros e. apply fromempty. apply n. apply e. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.