proposition: Lemma LRyamtab_spec_recip yam : yam \in LRyam_set P1 P2 P -> count_mem (val yam) (map to_word (LRyamtab_list P1 P2 P)) = 1.
proof: Proof. Proof using Hincl. rewrite inE => Hyam. have Hszyam : size yam = sumn (P / P1). by rewrite -evalseq_eq_size eval_yameval (sumn_diff_shape_intpartE P2). rewrite -[val yam](to_word_skew_reshape Hincl Hszyam). rewrite count_map. rewrite (eq_in_count (a2 := pred1 (skew_reshape P1 P (val yam)))); first last. move=> tab /= Htab; apply/eqP/eqP => [| -> //]. rewrite (to_word_skew_reshape Hincl Hszyam) => <-. have Hshape := (LRyamtab_shape (intpartnP P1) (intpartnP P) Hincl Htab). have <- : (outer_shape P1 (shape tab)) = P by rewrite Hshape diff_shapeK. rewrite skew_reshapeK //= -(size_map size tab) -/(shape tab) Hshape size_diff_shape. exact: size_included. apply (count_mem_LRyamtab_list (intpartnP P1) (intpartnP P) Hincl Hyam). - by rewrite (shape_skew_reshape Hincl Hszyam). - rewrite /is_yam_of_eval; rewrite (to_word_skew_reshape Hincl Hszyam). by rewrite yamevalP eval_yameval eq_refl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule