proposition: Lemma filter_gt_first_row0 n r t : is_tableau t -> dominate (head [::] t) r -> [seq x <- r | (x < n)%O] = [::] -> [seq [seq x <- i | (n <= x)%O] | i <- t] = t.
proof: Proof. Proof using. elim: t r => [// | t0 t IHt] /= r. move=> /and4P[_ Hrow Hdom Htab] Hdomr Hr. move/(count_gt_dominate n) : Hdomr. rewrite -!size_filter Hr /= leqn0 => /nilP Ht0. rewrite (IHt t0 Htab Hdom Ht0). rewrite (filter_le_row n Hrow). by rewrite -!size_filter Ht0 /= drop0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab