Lemma hzabsvalandnattohz ( n : nat ) : hzabsval ( nattohz n ) = n. Proof. induction n. - rewrite nattohzand0. rewrite hzabsval0. apply idpath. - rewrite nattohzandS. rewrite hzabsvalandplusnonneg. + rewrite hzabsvaland1. simpl. apply maponpaths. assumption. + rewrite <- (hzplusl0 1). apply hzlthtoleh. apply ( hzlthnsn 0 ). + rewrite <- nattohzand0. apply nattohzandleh. apply natleh0n. 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.