proposition: Lemma rem_corner_incr_nth sh i : is_part sh -> is_add_corner sh i -> is_rem_corner (incr_nth sh i) i.
proof: Proof. rewrite /is_add_corner /is_rem_corner /= nth_incr_nth. case: i => [/= | i]. case: sh => [// | s0 [// | s1 s]] /= /andP[]. by rewrite ltnS. move=> Hpart /orP[] //; rewrite [i.+1.-1]/=. elim: sh i Hpart => [| s0 sh IHsh] i /=; first by rewrite !nth_nil. move=> /andP[Hhead Hpart]. case: i => [_|i]. move: Hhead; case: sh Hpart {IHsh} => // s1 [| s2 sh] //= /andP[]. by rewrite ltnS. by move/(IHsh i Hpart). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype