proposition: Lemma hzabsvalandnattohz ( n : nat ) : hzabsval ( nattohz n ) = n.
proof: 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.
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