proposition: Lemma discr_prime_spec : forall n, prime_spec n (discr_prime n).
proof: Proof. move=>n. rewrite /prime_spec /discr_prime. by case: (prime n)=>//. Qed.
imports: mathcomp(ssreflect ssrfun eqtype ssrnat ssrbool prime eqtype)