proposition: Lemma hzdivhzabsval ( a b : hz ) ( p : hzdiv a b ) : natleh ( hzabsval a ) ( hzabsval b ) ∨ hzabsval b = 0%nat.
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble