proposition: Lemma hzminusplus (x y:hz) : -(x+y) = (-x) + (-y).
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra