Lemma hzqrandselfineq ( p : hz ) ( x : hzneq 0 p ) : hzleh 0 0 × hzlth 0 ( nattohz ( hzabsval p ) ). Proof. split. - apply isreflhzleh. - apply lemmas.hzabsvalneq0. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.