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