proposition: Lemma hzabsvaland1 : hzabsval 1 = 1%nat.
proof: Proof. apply ( invmaponpathsincl _ isinclnattohz ). rewrite hzabsvalgth0. - rewrite nattohzand1. apply idpath. - rewrite <- ( hzplusl0 1 ). apply ( hzlthnsn 0 ). 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