proposition: Lemma p'natEpi p n : n > 0 -> p^'.-nat n = (p \notin \pi(n)).
proof: Proof. by case: n => // n _; rewrite /pnat all_predC has_pred1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)