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