fact: Fixpoint bumprow r l : (option T) * (seq T) := if r is l0 :: r then if (l < l0)%O then (Some l0, l :: r) else let: (lr, rr) := bumprow r l in (lr, l0 :: rr) else (None, [:: l]).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab