proposition: Lemma p_part_gt1 p n : (n`_p > 1) = (p \in \pi(n)).
proof: Proof. by rewrite ltn_neqAle part_gt0 andbT eq_sym p_part_eq1 negbK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)