proposition: Lemma is_tableau_filter_gt t n : is_tableau t -> is_tableau (filter_gt_tab n t).
proof: Proof. Proof using. elim: t => [// | t0 t /= IHt] /and4P[Hnnil Hrow Hdom Htab]. case: ([seq x <- t0 | (x < n)%O] =P [::]) => /eqP Ht0 /=; first exact: IHt. rewrite Ht0 /=; apply/and3P; split; last exact: IHt. - apply sorted_filter; last exact Hrow. by move=> a b c; apply: le_trans. - rewrite (head_filter_gt_tab _ Htab). apply filter_gt_dominate => //=. by move: Htab; case t => [// | t1 t'] /= /and3P[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted