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