proposition: Lemma is_skew_tableau_filter_le n t: is_tableau t -> is_skew_tableau (shape (filter_gt_tab n t)) (filter_le_tab n t).
proof: Proof. Proof using. move=> Htab. rewrite is_skew_tableau_pad0 /filter_le_tab size_map. rewrite -(shape_inner_filter_le n Htab). exact: is_skew_tableau_filter_le_tmp. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab