proposition: Lemma head_lt_invins b s i : s != [::] -> invbump b s -> (head i s <= head i (invins b s))%O.
proof: Proof. Proof using. rewrite /invins /invbump; case: s => [// | l0 s /= _]. case (invbumprow b s) => r a. case: (leP b (head b s)) => _ //=. exact: ltW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab