proposition: Lemma filter_le_first_row0 n r t : is_tableau t -> dominate (head [::] t) r -> [seq x <- r | (x < n)%O] = [::] -> [seq [seq x <- i | (x < n)%O] | i <- t] = nseq (size 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. by rewrite Ht0 (IHt t0 Htab Hdom). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab