Lemma hzabsvalandplusneg ( n m : hz ) ( p : hzlth n 0 ) ( q : hzlth m 0 ) : hzabsval ( n + m ) = ( ( hzabsval n ) + ( hzabsval m ) )%nat. Proof. intros. assert ( hzlth ( n + m ) 0 ) as r. { rewrite <- ( hzrminus n ). change ( n - n ) with ( n + - n ). apply hzlthandplusl. apply ( istranshzlth _ 0 _ ). - assumption. - apply hzlth0andminus. assumption. } apply ( invmaponpathsincl _ isinclnattohz ). rewrite nattohzandplus. rewrite hzabsvallth0. - rewrite hzabsvallth0. + rewrite hzabsvallth0. * rewrite hzaddinvplus. apply idpath. * assumption. + assumption. - assumption. 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.