proposition: Lemma hzeqnmplusr' {n m i : hz} (e : ¬ (n = m)) (e' : n + i = m + i) : empty.
proof: Proof. apply e. exact (hzplusrcan _ _ i e'). Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra