fact: Fixpoint inspos r (l : T) : nat := if r is l0 :: r' then if (l < l0)%O then 0 else (inspos r' l).+1 else 0.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab