proposition: Lemma decr_nthK sh i : is_part sh -> is_rem_corner sh i -> incr_nth (decr_nth sh i) i = sh.
proof: Proof. rewrite /is_rem_corner. elim: sh i => [| s0 sh IHsh] /=; first by case. case=> [| i] /=; case: s0 => [| s0] //= /andP[]. - move=> {IHsh} Hs0 /part_head_non0 Hhead H ; case: s0 Hs0 H Hhead => //= _. by case: sh => //= s1 sh; rewrite ltnS leqn0 => /eqP ->. - by rewrite leqn0 => /part_head0F ->. by move=> Hhead Hpart Hnth; rewrite IHsh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype