proposition: Lemma part_eqP p q : is_part p -> is_part q -> reflect (forall i, nth 0 p i = nth 0 q i) (p == q).
proof: Proof. move=> Hp Hq. apply (iffP idP) => [/eqP -> //| H]. apply/eqP; apply (eq_from_nth (x0 := 0)); last by move=> i _; exact: H. move: H Hp Hq. wlog Hpq : p q / (size p) <= (size q). move=> Hwlog Hnth. by case: (leqP (size p) (size q)) => [|/ltnW] /Hwlog /[apply]/[apply] ->. move=> Hnth /is_part_ijP[Hlastp Hp] /is_part_ijP[Hlastq Hq]. apply anti_leq; rewrite {}Hpq /=. case: q Hnth Hlastq Hq => //= q0 q Hnth Hlastq Hq. rewrite leqNgt; apply/negP => Habs. move: Hlastq. have:= Habs; rewrite -(ltn_predK Habs) ltnS => /(Hq _ _). by rewrite nth_last /= -Hnth nth_default // leqn0 => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype