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