Lemma hzdivandmultl ( a c d : hz ) ( p : hzdiv d a ) : hzdiv d ( c * a ). Proof. intros. intros P s. use (hinhuniv _ p). intro k. destruct k as [ k f ]. apply s. unfold hzdiv0. split with ( c * k ). rewrite ( hzmultcomm d ). rewrite hzmultassoc. unfold hzdiv0 in f. rewrite ( hzmultcomm k ). rewrite f. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.