Lemma hzabsvalneq0 ( n : hz ) ( p : hzneq 0 n ) : hzlth 0 ( nattohz ( hzabsval n ) ). Proof. intros. destruct ( hzneqchoice 0 n p ) as [ left | right ]. - rewrite hzabsvallth0. + apply hzlth0andminus. apply left. + apply left. - rewrite hzabsvalgth0. + assumption. + apply right. 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.