Lemma hzdivhzabsval ( a b : hz ) ( p : hzdiv a b ) : natleh ( hzabsval a ) ( hzabsval b ) ∨ hzabsval b = 0%nat. Proof. intros P q. apply ( p P ). intro t. destruct t as [ k f ]. unfold hzdiv0 in f. apply q. apply natdivleh with ( hzabsval k ). rewrite hzabsvalandmult. rewrite f. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.