proposition: Lemma is_part_incr_first_n sh n : is_part sh -> is_part (incr_first_n sh n).
proof: Proof. elim: sh n => [// n _| s0 sh IHsh] /=; first exact: is_part_nseq1. case=> //= n /andP[Hhead {}/IHsh /= ->]; rewrite andbT. case: sh Hhead => [_ | s1 sh] /=; first by case n. case: n => [| n] /=; last by apply. by move/leq_trans; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype