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