proposition: Lemma eq_in_partn pi1 pi2 n : {in \pi(n), pi1 =i pi2} -> n`_pi1 = n`_pi2.
proof: Proof. by move=> pi12; apply/eqP; rewrite eqn_dvd ?sub_in_partn // => p /pi12->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)