Lemma hzdichot {m n} : neg (nattohz m = - nattohz (S n)). 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.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.