proposition: Lemma is_part_incr_nth_size sh i : is_part sh -> is_part (incr_nth sh i) -> i <= size sh.
proof: Proof. elim: sh i => [| sh0 sh IHsh] /= i. by move=> _; case: i => //= i /andP[]; rewrite leqn0 => /part_head0F ->. case: i => // i. by rewrite ltnS /= => /andP[_ /IHsh H] /andP[_ /H]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype