proposition: Lemma LRyamtab_all : all (is_yam_of_eval P2) (map to_word (LRyamtab_list P1 P2 P)).
proof: Proof. Proof using Hincl. by apply/allP => w /mapP[tab /LRyamtabP Htab ->]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule