proposition: Lemma pi_pnat pi p n : p.-nat n -> p \in pi -> pi.-nat n.
proof: Proof. move=> p_n pi_p; have [n_gt0 _] := andP p_n. by apply/pnatP=> // q q_pr /(pnatP _ n_gt0 p_n _ q_pr)/eqnP->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)