fact: Fixpoint last_big t b := if t is t0 :: t' then if last b t0 == b then 0 else (last_big t' b).+1 else 0.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau