proposition: Lemma hzdivand0 ( n : hz ) : hzdiv n 0.
proof: Proof. intros. intros P s. apply s. split with 0. unfold hzdiv0. apply hzmultx0. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble