proposition: Lemma incr_nthK sh i : is_part sh -> is_part (incr_nth sh i) -> decr_nth (incr_nth sh i) i = sh.
proof: Proof. elim: sh i => [| s0 sh IHsh] [| i] //=. - by move=> _ /andP[]; rewrite leqn0 => /part_head0F ->. - by case: s0 => //= /andP[]; rewrite leqn0 => /part_head0F ->. - move=> /andP[Head Hpart] /andP[Headincr Hpartincr]. by rewrite IHsh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype