proposition: Lemma bumprow_count p : let: (lr, tr) := bumpRow in count p Row + (p l) == count p tr + if lr is Some ll then (p ll) else 0.
proof: Proof. Proof using. elim: Row => [| t0 r IHr] /=; first by rewrite !addn0. case: (ltP l t0) => _ /=. - by rewrite addnC -addnA eqn_add2l addnC eqn_add2l. - move: IHr; case (bumprow r l) => [tr lr] /= IHr. by rewrite -!addnA eqn_add2l. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab