proposition: Lemma head_leq_invbumped b s : s != [::] -> is_row s -> (head inh s <= (invbumped b s))%O.
proof: Proof. Proof using. rewrite /invbumped. elim: s => [_ // | l0 s IHs] /= _ /is_row_cons[Hhead Hrow]. case: (s =P [::]) => [-> /= | /eqP Hnnil]; first by rewrite lexx. rewrite (set_head_default inh _ Hnnil). case: (leP b (head inh s)) => [/= | _]; first by rewrite lexx. move: {IHs} (IHs Hnnil Hrow). case H : (invbumprow b s) => [r a] /= Hb. apply: (le_trans Hhead). by rewrite (set_head_default inh _ Hnnil). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab