Lemma hzaddinvplus ( n m : hz ) : - ( n + m ) = ( - n ) + ( - m ). Proof. intros. apply commringaddinvunique with ( a := n + m ). - apply ringrinvax1. - assert ( ( n + m ) + ( - n + - m ) = n + - n + m + - m ) as i. { assert ( n + m + ( - n + - m ) = n + ( m + ( - n + - m ) ) ) as i0 by apply ringassoc1. assert ( n + ( m + ( - n + - m ) ) = n + ( m + - n + - m ) ) as i1. { apply maponpaths. apply pathsinv0. apply ringassoc1. } assert ( n + ( m + - n + - m ) = n + (- n + m + - m ) ) as i2. { apply maponpaths. apply ( maponpaths ( fun x => x + - m ) ). apply ringcomm1. } assert ( n + ( - n + m + - m ) = n + ( - n + m ) + - m ) as i3. { apply pathsinv0. apply ringassoc1. } assert ( n + ( - n + m ) + - m = n + - n + m + - m ) as i4. { apply pathsinv0. apply ( maponpaths ( fun x => x + - m ) ). apply ringassoc1. } exact ( pathscomp0 i0 ( pathscomp0 i1 ( pathscomp0 i2 ( pathscomp0 i3 i4 ) ) ) ). } assert ( n + - n + m + -m = 0 ) as j. { assert ( n + - n + m + - m = 0 + m + - m ) as j0. { apply ( maponpaths ( fun x => x + m + - m ) ). apply ringrinvax1. } assert ( 0 + m + - m = m + - m ) as j1. { apply ( maponpaths ( fun x => x + - m ) ). apply ringlunax1. } assert ( m + - m = 0 ) as j2 by apply ringrinvax1. exact ( pathscomp0 j0 ( pathscomp0 j1 j2 ) ). } exact ( pathscomp0 i j ). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.