proposition: Lemma is_skew_tableau_filter_le_tmp n t : is_tableau t -> is_skew_tableau (shape ([seq [seq x <- i | (x < n)%O] | i <- t])) (filter_le_tab n t).
proof: Proof. Proof using. elim: t => [// | t0 t IHt] /= /and4P[Hnnil Hrow Hdom Htab]. apply/and4P; split. - rewrite !size_filter /=. set p1 := (X in count X); set p2 := (X in _ + count X _). have /eq_count -> : p2 =1 predC p1 by move=> i /=; rewrite -leNgt. rewrite count_predC. by move: Hnnil; apply contra => /nilP ->. - apply sorted_filter; last exact Hrow. by move=> a b c; exact: le_trans. - case: t Hdom Htab {IHt} => [// | t1 t] /= Hdom /and4P[_ Hrow1 _ _] {t}. rewrite !size_filter. exact: filter_le_dominate. - exact: IHt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab