proposition: Lemma yamtab_shift_countE inn0 innev shape sh row sol : is_part inn0 -> is_row (row ++ sol) -> size row = sh -> is_skew_yam inn0 innev sol -> is_skew_yam innev shape row -> included shape outev -> count (preim (fst (B:=seq nat)) (pred1 (row ++ sol))) (yamtab_shift innev (head (size inn0) sol) sh sol) = 1.
proof: Proof. Proof using . move=> Hinn0. elim : sh row sol shape => [| sh IHsh ] row sol shape /= Hisrow. by move=> /eqP/nilP -> _ /=; rewrite eq_refl. case: row Hisrow => [// |r0 row] Hisrow /=. move/eqP; rewrite eqSS => /eqP Hsize Hskew0 Hskew Hincl. have Hinn := is_part_skew_yam Hinn0 Hskew0. rewrite count_flatten -map_comp. set f1 := (X in map X); set rec := (X in map _ X). pose f2 := nat_of_bool \o (pred1 (row ++ sol)) \o (@fst (seq nat) (seq nat)). have : {in rec, f1 =1 f2}. rewrite /rec /f1 /f2 {rec f1 f2} => [[r shr]] /= Hr. rewrite count_map. case: (r =P (row ++ sol)) => [Heq | /eqP/negbTE Hneq] /=. - subst r. rewrite (eq_count (a2 := pred1 r0)); first last. by move=> i /=; rewrite eqseq_cons eq_refl andbT. rewrite (_ : head _ _ = head (size inn0) (row ++ sol)); first last. by case row => //=; case sol. apply: (choose_one_countE Hinn0 (yamtab_shiftP Hskew0 Hr) (skew_yam_cat Hskew0 Hskew) Hincl _ Hisrow). rewrite /=. exact: head_row_skew_yam Hinn0 Hisrow (skew_yam_cat Hskew0 Hskew). - rewrite (eq_count (a2 := pred0)); first by rewrite count_pred0. by move=> y /=; rewrite eqseq_cons Hneq andbF. rewrite eq_in_map /rec /f2 => -> {f1 f2 rec}. rewrite sumn_count /=. apply: (IHsh _ _ _ (is_row_consK Hisrow) Hsize Hskew0 (skew_yam_consK Hinn Hskew)). apply: (included_trans _ Hincl). exact: included_decr_nth. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule