proposition: Lemma hzeqissi {i : hz} (e : hzeq i (i + 1 + 1)) : empty.
proof: Proof. set (tmp := hzbooleqissi i). cbn in e. rewrite <- e in tmp. rewrite (hzeqbooleqii i) in tmp. apply nopathstruetofalse. apply tmp. Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra