proposition: Lemma yamtab_rows_countE innev shape row base : is_part innev -> size row = size base -> dominate row base -> is_row row -> is_skew_yam innev shape row -> included shape outev -> count (preim (fst (B:=seq nat)) (pred1 row)) (yamtab_rows innev base) = 1.
proof: Proof. Proof using . move=> Hinn. elim: row base shape => [| l0 row IHrow] [| b0 base] //= shape. move/eqP; rewrite eqSS => /eqP Hsize Hdom Hisrow Hskew Hincl. 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) \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) => [Hrow | /eqP/negbTE Hneq] /=. - subst r. rewrite (eq_count (a2 := pred1 l0)); first last. by move=> i /=; rewrite eqseq_cons eq_refl andbT. apply: (choose_one_countE Hinn (yamtab_rowsP Hr) Hskew Hincl _ Hisrow). have /dominate_head/(_ Hdom) : l0 :: row != [::] by []. rewrite ltEnat /= => -> /=. exact: head_row_skew_yam Hinn Hisrow 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: (IHrow _ _ Hsize (dominate_tl Hdom) (is_row_consK Hisrow) (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