Lemma hzdivistrans : istrans hzdiv. Proof. intros a b c p q. use (hinhuniv _ p). intro k. destruct k as [ k f ]. use (hinhuniv _ q). intro l. destruct l as [ l g ]. intros P s. apply s. unfold hzdiv0 in f, g. split with ( k * l ). red. rewrite <- hzmultassoc. rewrite f. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.