proposition: Lemma rem_corner_incr_first_n sh i : is_part sh -> is_rem_corner (incr_first_n sh i.+1) i.
proof: Proof. rewrite /is_rem_corner. elim: sh i => [/= i _ | s0 sh IHsh i]; first by elim: i. move=> /= => /andP[Hhead {}/IHsh Hrec]. case: i => [| i] /=; first by case: sh Hhead {Hrec}. exact: (Hrec i). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype