proposition: Lemma hzdichot {m n} : neg (nattohz m = - nattohz (S n)).
proof: Proof. intros. intro e. assert (d := maponpaths hzsign e); clear e. rewrite hzsign_hzsign in d. assert( f := maponpaths (λ i, nattohz m + i) d); simpl in f; clear d. change (nattohz m + - nattohz m) with (nattohz m - nattohz m) in f. rewrite hzrminus in f. change (0 = nattohz (m + S n)) in f. assert (g := nattohz_inj f); clear f. rewrite natpluscomm in g. exact (negpaths0sx _ g). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra