proposition: Lemma res_tabK (t : Tm) : shape (filter_gt_tab sz t) == la -> eqeval t (rcons s m) -> ext_tab (res_tab t) = t.
proof: Proof. rewrite /ext_tab => Hsh Hev; apply val_inj => /=. rewrite /ext_tab_fun eval_res_tab //. rewrite /res_tab (insubT _ (res_tabP Hsh)) /=. rewrite -[RHS](join_tab_filter sz (tabshP t)); congr join_tab. rewrite -[RHS](skew_reshapeK (inner := shape (filter_gt_tab sz t))); first last. rewrite /shape size_map /filter_gt_tab /filter_le_tab. rewrite size_map /= size_filter; apply: (leq_trans (count_size _ _)). by rewrite size_map. move: Hsh => /eqP Hsh. congr skew_reshape. - by rewrite Hsh. - suff -> : shape (filter_le_tab sz t) = mu / (shape (filter_gt_tab sz t)). rewrite diff_shapeK // -(shape_tabsh t); apply: included_shape_filter_gt. exact: tabshP. apply (eq_from_nth (x0 := 0)). - by rewrite size_diff_shape /filter_le_tab -(shape_tabsh t) !size_map. - move=> i; rewrite /shape !size_map => Hi. rewrite -diff_shape_pad0 nth_diff_shape !nth_shape -/(shape _). rewrite -(shape_tabsh t) size_map. rewrite -shape_inner_filter_le //= nth_shape !(nth_map [::]) ?size_map //. rewrite !size_filter -(count_predC (>%O sz) (nth [::] t i)). rewrite addKn; apply eq_count => x /=. by rewrite -leNgt. - have Hw : size (to_word (filter_le_tab sz t)) = m. rewrite -filter_le_to_word size_filter -sum_count_mem /=. rewrite (bigD1 sz) /= // (eqevalP _ Hszrcons Hev). rewrite nth_rcons ltnn eq_refl big1 ?addn0 // => i. rewrite andbC -lt_def ltEord /= => Hi. rewrite (eqevalP _ Hszrcons Hev) nth_rcons. by rewrite ltnNge (ltnW Hi) (gtn_eqF Hi). rewrite -{1}Hw; symmetry; apply/all_pred1P/allP => /= i. rewrite /to_word => /flattenP[/= rtmp]. rewrite mem_rev => /mapP[/= r Hr ->{rtmp}]. rewrite mem_filter leEord => /andP[/= Hi Hir]. apply/eqP/val_inj => /=; apply anti_leq; rewrite {}Hi andbT. have /count_memPn/eqP : i \in to_word t. by rewrite /to_word; apply/flattenP; exists r; first rewrite mem_rev. rewrite (eqevalP _ Hszrcons Hev); apply contraR; rewrite -ltnNge => Hi. by rewrite nth_default // size_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn