proposition: Lemma included_shape_filter_gt c (t : seq (seq T)) : is_tableau t -> included (shape (filter_gt_tab c t)) (shape t).
proof: Proof. move=> Ht; rewrite /filter_gt_tab. elim: t Ht => [// | t0 t IHt] /and4P[Hnnil Hrow Hdom Htab] /=. case: ([seq x <- t0 | (x < c)%O] =P [::]) => [Hhead | _] /=. - rewrite (filter_le_first_row0 Htab Hdom Hhead). suff -> : [seq r <- nseq (size t) [::] | r != [::]] = [::] by []. by move=> T0; elim: (size t). - rewrite (IHt Htab) andbT. by rewrite size_filter; apply: (leq_trans (count_size _ _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab