Lemma nozerodiv ( n : hz ) ( i : hzneq 0 n ) : neg ( hzdiv 0 n ). Proof. intros. intro p. unfold hzneq in i. simpl in i. apply i. apply ( p ( make_hProp ( 0 = n ) ( isasethz 0 n ) ) ). intro t. destruct t as [ k f ]. unfold hzdiv0 in f. rewrite ( hzmult0x ) in f. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.