proposition: Lemma join_tab_filter n t : is_tableau t -> join_tab (filter_gt_tab n t) (filter_le_tab n t) = t.
proof: Proof. Proof using. rewrite /join_tab. elim: t => [// | t0 t IHt] /= /and4P[Hnnil Hrow0 Hdom Htab]. case H: [seq x <- t0 | (x < n)%O] => [| f0 f] /=. - rewrite {IHt} (filter_le_first_row0 Htab Hdom H). rewrite [filter _ _](_ : _ = [::]); last by elim: (size t). rewrite cat0s /= (filter_le_row n Hrow0) -!size_filter /= H /= drop0. congr (_ :: _). rewrite (filter_gt_first_row0 Htab Hdom H). by elim: t {Hdom Htab H Hrow0 Hnnil} => [// | t1 t] /= ->. - rewrite (IHt Htab) (filter_le_row _ Hrow0). rewrite -[f0 :: _ ++ _]cat1s catA cat1s -H. by rewrite (filter_gt_row _ Hrow0) cat_take_drop. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab