proposition: Lemma isapropisaprime ( p : hz ) : isaprop ( isaprime p ).
proof: Proof. intros. apply isofhleveldirprod. - apply ( hzlth 1 p ). - apply impred. intro m. apply impredfun. apply ( m = 1 ∨ m = p ). Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble