proposition: Lemma hzdivandmultr ( a c d : hz ) ( p : hzdiv d a ) : hzdiv d ( a * c ).
proof: Proof. intros. rewrite hzmultcomm. apply hzdivandmultl. assumption. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble