proposition: Lemma hb_strip_shape_res_tab (t : Tm) : eqeval t (rcons s m) -> hb_strip (shape_res_tab t) mu.
proof: Proof. rewrite /shape_res_tab => Hev. apply/hb_stripP => // i. rewrite [nth 0 (IntPartN _) _]/= Hev. have := shape_inner_filter_le sz (tabshP t) => /(congr1 (fun s => nth 0 s i)). rewrite nth_pad => <-. case: (ssrnat.ltnP i.+1 (size t)) => Hi. - rewrite /shape !(nth_map [::]) ?size_map //; try by apply ltnW. apply/andP; split; first last. move/ltnW in Hi. by rewrite -(shape_tabsh t) nth_shape size_filter; apply: count_size. have:= tabshP t => /is_tableauP[_ /(_ i) Hrow]. move=> /(_ _ _ (ltnSn i))/dominateP[]. rewrite -(shape_tabsh t) nth_shape. move Hr : (nth [::] t i) Hrow => r. move Hr1 : (nth [::] t i.+1) => r1 Hrow Hszle Hdom. rewrite size_filter. case: leqP => // Hleq; move/(_ _ Hleq): Hdom. move: Hi => /(mem_nth [::]); rewrite Hr1 => Hi. set xabs := nth inh r1 (count (>%O sz) r). have /count_memPn/eqP : xabs \in to_word t. rewrite /to_word; apply/flattenP; exists r1; first by rewrite mem_rev. by apply: mem_nth. rewrite (eqevalP _ Hszrcons Hev) nth_rcons. case: (ssrnat.leqP xabs (size s)) => [Hxabs _ | Hxabs]; first last. by rewrite (gtn_eqF Hxabs) ltnNge (ltnW Hxabs). rewrite ltEord /= => /leq_trans/(_ Hxabs) {xabs Hxabs}. have size_take_leq l sq : size (take l sq) <= size sq. by rewrite size_take; case ssrnat.ltnP => [/ltnW|]. move/(_ _ (count (<%O sz) r) r): size_take_leq => HHH. have := leq_trans Hleq Hszle. rewrite -{2 3}(cat_take_drop (count (>%O sz) r) r) nth_cat. rewrite size_take (leq_trans Hleq Hszle) ltnn subnn. rewrite size_cat size_take (leq_trans Hleq Hszle). rewrite -addn1 leq_add2l -(filter_le_row sz Hrow) => /(mem_nth inh). move: (nth _ _ _) => xabs. rewrite mem_filter /= leEord andbC => /andP[_] /=. move=>/leq_ltn_trans H1/H1. by rewrite ltnn. - rewrite nth_default -(shape_tabsh t) ?size_map //=. case: (ssrnat.ltnP i (size t)) => {}Hi. + rewrite !(nth_map [::]) ?size_map //. by rewrite size_filter; apply: (leq_trans (count_size _ _)). + by rewrite !nth_default ?size_map. 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