proposition: Lemma conj_part_ind sh l : sh != [::] -> is_part sh -> l >= size sh -> conj_part (incr_first_n sh l) = l :: conj_part sh.
proof: Proof. elim: sh l => //= s0 s IHs l _ /=. move=> /andP[_ Hpart] Hs0. case: l Hs0 => //= l; rewrite ltnS => Hs0. case: s IHs Hpart Hs0 => [// | s1 s IHs]. - by case: l => [// | l]; rewrite conj_nseq; last exact: ltn0Sn. - have Hneq : s1 :: s != [::] by []. move=> Hpart Hsize /=. move/(_ l Hneq Hpart Hsize) : IHs. by case: l Hsize => //= l _ ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype