Lemma hzminusplus (x y:hz) : -(x+y) = (-x) + (-y). Proof. intros. apply (hzplusrcan _ _ (x+y)). rewrite hzlminus. rewrite (hzpluscomm (-x)). rewrite (hzplusassoc (-y)). rewrite <- (hzplusassoc (-x)). rewrite hzlminus. rewrite hzplusl0. rewrite hzlminus. reflexivity. Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.