proposition: Lemma sub_in_pnat pi rho n : {in \pi(n), {subset pi <= rho}} -> pi.-nat n -> rho.-nat n.
proof: Proof. rewrite /pnat => subpi /andP[-> pi_n]. by apply/allP=> p pr_p; apply: subpi => //; apply: (allP pi_n). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)