Lemma isaprimetoneq0 { p : hz } ( x : isaprime p ) : hzneq 0 p. Proof. intros. intros f. apply ( isirreflhzlth 0 ). apply ( istranshzlth _ 1 _ ). - apply hzlthnsn. - rewrite f. apply ( pr1 x ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.