Lemma hzabsvalandplusnonneg ( n m : hz ) ( p : hzleh 0 n ) ( q : hzleh 0 m ) : hzabsval ( n + m ) = ( ( hzabsval n ) + ( hzabsval m ) )%nat. Proof. intros. assert ( hzleh 0 ( n + m ) ) as r. { rewrite <- ( hzrminus n ). change ( n - n ) with ( n + - n ). apply hzlehandplusl. apply ( istranshzleh _ 0 _ ). - apply hzgeh0andminus. apply p. - assumption. } apply ( invmaponpathsincl _ isinclnattohz ). rewrite nattohzandplus. rewrite hzabsvalgeh0. - rewrite hzabsvalgeh0. + rewrite hzabsvalgeh0. * 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.