proposition: Lemma eqevalP n (t : (seq (seq 'I_n.+1))) (la : seq nat) : size la <= n.+1 -> reflect (forall i : 'I_n.+1, count_mem i (to_word t) = nth 0 la i) (eqeval t la).
proof: Proof. rewrite /eqeval /eval /mpart => ->. apply (iffP eqP) => [Heq i| Hcount]. - by move: Heq => /(congr1 (fun t => tnth t i)); rewrite !tnth_mktuple. - by apply eq_from_tnth => i; rewrite !tnth_mktuple. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn