proposition: Lemma hzabsvalandplusnonneg ( n m : hz ) ( p : hzleh 0 n ) ( q : hzleh 0 m ) : hzabsval ( n + m ) = ( ( hzabsval n ) + ( hzabsval m ) )%nat.
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids