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