fact: Fixpoint instabnrow t l : seq (seq T) * nat := if t is t0 :: t then let: (lr, rr) := bumprow t0 l in if lr is Some ll then let: (tres, nres) := instabnrow t ll in (rr :: tres, nres.+1) else (rr :: t, 0) else ([:: [:: l]], 0).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab