proposition: Lemma rem_corner_incr_first_nE sh n i : is_part sh -> is_rem_corner sh i -> is_rem_corner (incr_first_n sh n) i.
proof: Proof. rewrite /is_rem_corner. elim: sh i n => [/= i n _ | s0 sh IHsh i n]; first by elim: i. rewrite [is_part _]/= => /andP[Hhead Hpart]. case: i => [/= | i]. case: sh IHsh Hhead Hpart => [// | s1 sh] IHsh Hhead Hpart H10. by case: n {IHsh Hhead Hpart} => [| [| n]]. case: n {IHsh Hhead Hpart} => [| [| n]] //=. exact: (leq_trans H10). rewrite [X in (X -> _)]/= => Hcorn. case: n => //= n. exact: (IHsh _ n Hpart Hcorn). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype