proposition: Lemma pi_p'nat p pi n : pi.-nat n -> p \in pi^' -> p^'.-nat n.
proof: Proof. by move=> pi_n; apply: pi'_p'nat; rewrite pnatNK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)