proposition: Lemma LRyam_spec_recip yam : yam \in LRyam_set P1 P2 P -> count_mem yam LRyam_list = 1.
proof: Proof. Proof using Hincl. move=> /LRyamtab_spec_recip Hyam. rewrite (eq_count (a2 := pred1 (val yam) \o val)); last by []. by rewrite -count_map subType_seqP // LRyamtab_all. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule