Definition isaprime ( p : hz ) : UU := hzlth 1 p × forall m : hz, hzdiv m p -> m = 1 ∨ m = p.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.