proposition: Lemma is_part_decr_nth sh i : is_part sh -> is_rem_corner sh i -> is_part (decr_nth sh i).
proof: Proof. rewrite /is_rem_corner. elim: sh i => [| s0 sh IHsh] /=; first by case. case=> [| i] /=. case: s0 => [| [| s0]] //= /andP[_ ->]. by case sh => //= s1 _; rewrite ltnS => ->. move=> /andP[Hhead Hpart] Hnth. apply/andP; split; last exact: IHsh. apply: (@leq_trans (head 1 sh)); last exact Hhead. case: sh {IHsh Hhead Hnth s0} Hpart => [// | s1 s]; first by case i. case i => //= /andP[]. case: s1 => [| [| s1]] //=. by rewrite leqn0 => /part_head0F ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype