proposition: Lemma sumn_take_inj s t : is_part s -> is_part t -> (forall k, sumn (take k s) = sumn (take k t)) -> s = t.
proof: Proof. elim: s t => [t _ | s0 s IHs t]. - move/part_head_non0; case: t => //= t0 t Ht0 IHs. exfalso; move/(_ 1) : IHs; rewrite /= take0 /= addn0 => H. by rewrite H eq_refl in Ht0. - case: t s IHs => [s _ Hs _ /(_ 1) | t0 t] /=. + rewrite take0 /= addn0 => Hs0. by exfalso; move/part_head_non0 : Hs; rewrite Hs0. + move=> s IHs /is_part_consK Hps /is_part_consK Hpt /= Heq. have:= Heq 1; rewrite /= !take0 /= !addn0 => Ht0; subst t0. congr (s0 :: _); apply: (IHs _ Hps Hpt). move=> k; move/(_ k.+1) : Heq. by move=> /= /eqP; rewrite eqn_add2l => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype