proposition: Lemma eq_in_pnat pi rho n : {in \pi(n), pi =i rho} -> pi.-nat n = rho.-nat n.
proof: Proof. by move=> eqpi; apply/idP/idP; apply: sub_in_pnat => p /eqpi->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)