proposition: Lemma shape_inner_filter_le n t : is_tableau t -> shape ([seq [seq x <- i | (x < n)%O] | i <- t]) = pad 0 (size t) (shape (filter_gt_tab n t)).
proof: Proof. Proof using. rewrite /pad /=. elim: t => [// | t0 t IHt] /= /and4P[Hnnil0 Hrow0 Hdom Htab]. case: ([seq x <- t0 | (x < n)%O] =P [::]) => Ht0 /=; first last. by rewrite subSS -(IHt Htab). rewrite Ht0 /= {IHt}. rewrite (filter_le_first_row0 Htab Hdom Ht0). rewrite [filter _ _ ](_ : _ = [::]); last by elim: (size t). by rewrite /= /shape map_nseq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab