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