proposition: Lemma hzeqisi {i : hz} (e' : hzeq i (i + 1)) : empty.
proof: Proof. apply nopathstruetofalse. rewrite <- (hzbooleqisi i). rewrite <- e'. apply (! (hzeqbooleqii i)). Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra