proposition: Lemma count_instab t l p : is_tableau t -> count p (to_word (instab t l)) = (p l) + count p (to_word t).
proof: Proof. Proof using. elim: t l => [// _ | r t IHt] l /= /and4P[_ _ _ Htab]. have:= bumprow_count r l p. case (bumprow r l) => [[ll|] lr] /= /eqP Hbump; rewrite addnC in Hbump; rewrite !to_word_cons !count_cat [_ + (count p r)]addnC addnA Hbump. - by rewrite (IHt ll Htab) -addnA addnC -addnA addnC. - by rewrite addn0 addnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab