proposition: Lemma LRyamtab_list_countE innev inner sh0 row0 yamtab : is_part innev -> sorted geq (sh0 :: inner) -> is_part (sh0 + size row0 :: (outer_shape inner (shape yamtab))) -> size inner = size yamtab -> is_skew_tableau (sh0 :: inner) (row0 :: yamtab) -> is_skew_yam innev outev (to_word yamtab) -> count_mem yamtab (LRyamtab_list_rec innev inner (outer_shape inner (shape yamtab)) sh0 row0) = 1.
proof: Proof. Proof using . elim: yamtab innev inner sh0 row0 => [// | row1 yamtab IHyamtab] innev [// | inn0 inn] sh0 row0 Hinnev. by move=> _ _ /eqP/nilP -> /=. move=> Hinn Hout Hsize Hskew Hyam. rewrite /= in Hsize; move: Hsize => /eqP; rewrite eqSS => /eqP Hsize. have Hskewrec : is_skew_tableau (inn0 :: inn) (row1 :: yamtab). by move: Hskew => /=/and4P[]. move/(_ _ inn inn0 row1 _ (path_sorted Hinn) (is_part_consK Hout) Hsize Hskewrec) : IHyamtab => Hrec. rewrite /= count_flatten -map_comp subSS -/(outer_shape _ _). set f1 := (X in map X); set rec := (X in map _ X). pose f2 := nat_of_bool \o (pred1 row1) \o (@fst (seq nat) (seq nat)). have : {in rec, f1 =1 f2}. rewrite /rec /f1 /f2 {rec f1 f2} => [[rshift shrshift]] /= Hrshift. rewrite count_map /=. case: (rshift =P row1) => [Hrow1 | /eqP/negbTE Hneq] /=. - rewrite Hrow1 (eq_count (a2 := pred1 yamtab)); first last. by move => y /=; rewrite eqseq_cons eq_refl /=. move: Hyam; rewrite to_word_cons. move: Hrshift=>/flatten_mapP[[row shrow] /yamtab_rowsP/yamtab_shiftP H{}/H]. rewrite Hrow1 => Hsk1 Hsk2. apply (Hrec shrshift (is_part_skew_yam Hinnev Hsk1)). exact: (skew_yam_catrK Hinnev Hsk1 Hsk2). - rewrite (eq_count (a2 := pred0)); first by rewrite count_pred0. by move=> y /=; rewrite eqseq_cons Hneq. rewrite eq_in_map /rec /f2 => -> {f1 f2 rec Hrec}. rewrite !map_comp map_flatten -!map_comp sumn_count. rewrite count_flatten -map_comp. set f1 := (X in map X); set rowl := (X in map _ X). pose f2 := nat_of_bool \o (pred1 (drop (sh0 - inn0) row1)) \o (@fst (seq nat) (seq nat)). have : {in rowl, f1 =1 f2}. rewrite /rowl /f1 /f2 {rowl f1 f2} => [[row shrow]] /= Hrow. rewrite count_map /=. case: (row =P (drop (sh0 - inn0) row1)) => [Hrow1 | /eqP/negbTE Hneq] /=. - have Hshrow := yamtab_rowsP Hrow. rewrite -(cat_take_drop (sh0 - inn0) row1) -Hrow1. move: Hyam; rewrite to_word_cons =>/(skew_yam_catK Hinnev) [shrow1 Hshrow1]. move=> /(skew_yam_included (is_part_skew_yam Hinnev Hshrow1)) Hincl. apply: (yamtab_shift_countE Hinnev _ _ Hshrow _ Hincl). + rewrite Hrow1 cat_take_drop. by move: Hskew => /= /and5P[_ _ _ _ /andP[]]. + rewrite size_cat Hrow1 -size_cat cat_take_drop size_take -/(minn _ _). move: Hinn => /= /andP[H0 _]. by rewrite -{2}[sh0](subnKC H0) -addn_minr addKn. + move: Hshrow; rewrite Hrow1 => /(skew_yam_catrK Hinnev) H. move: Hshrow1; rewrite -{1}(cat_take_drop (sh0 - inn0) row1). exact: H. - rewrite (eq_in_count (a2 := pred0)); first by rewrite count_pred0. move=> [shift shshift] /yamtab_shift_drop /= Hshift. move: Hneq; apply contraFF. rewrite -Hshift => /eqP ->. case: (leqP sh0 (inn0 + size row1)) => [_ // | /ltnW Hover]. have:= leq_sub2r inn0 Hover; rewrite addKn => /drop_oversize ->. by rewrite drop_oversize. rewrite eq_in_map /rowl /f2 => -> {f1 f2 rowl}. rewrite map_comp sumn_count count_map /=. move: Hyam; rewrite to_word_cons -{1}(cat_take_drop (sh0 - inn0) row1) catA => Hyam. have:= skew_yam_catK Hinnev Hyam => [] [shape Hdrop]. move=> /(skew_yam_included (is_part_skew_yam Hinnev Hdrop)) Hshape. have Heq : size (drop (sh0 - inn0) row1) = size (take (inn0 + size row1 - sh0) row0). rewrite size_drop size_takel. - by move: Hinn => /= /andP[/subnBA -> _]; rewrite addnC. - move: Hout => //= /andP[/(leq_sub2r sh0)]. by rewrite addKn addnC => -> _. apply: (yamtab_rows_countE Hinnev Heq _ (is_row_drop _ _) Hdrop Hshape). - move: Hskew => /= /and4P[_ _]; rewrite skew_dominate_cut /skew_dominate => Hdom _. suff <- : size row1 - (sh0 - inn0) = inn0 + size row1 - sh0 by exact Hdom. move: Hinn => /= /andP[/subnBA -> _]. by rewrite addnC. - by move: Hskew => /= /and5P[_ _ _ _ /andP[]]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule