proposition: Lemma head_filter_gt_tab n t : is_tableau t -> head [::] (filter_gt_tab n t) = [seq x <- head [::] t | (x < n)%O].
proof: Proof. Proof using. elim: t => [// | t0 t /= IHt] /and4P[Hnnil0 Hrow0 Hdom Htab]. case: ([seq x <- t0 | (x < n)%O] =P [::]) => Ht0 //=. rewrite (IHt Htab) Ht0 {IHt}. case: t Hdom Htab => [// | t1 t] /= Hdom /and3P[Hnnil1 Hrow1 _]. have /dominateP[] := filter_gt_dominate n Hrow0 Hrow1 Hdom. by rewrite Ht0 /= leqn0 => /nilP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted