proposition: Lemma hzabsvalandplusneg ( n m : hz ) ( p : hzlth n 0 ) ( q : hzlth m 0 ) : hzabsval ( n + m ) = ( ( hzabsval n ) + ( hzabsval m ) )%nat.
proof: 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.
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