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