proposition: Lemma isdecrelhzeqpii (i : hz) : isdecrelhzeq (i - 1) i = ii2 (fun (e : hzeq (i - 1) i) => hzeqpii e).
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra