proposition: Lemma invbump_geq_head t tin l nrow : t != [::] -> is_tableau t -> invinstabnrow t nrow = (tin, l) -> (l >= head l (head [::] t))%O.
proof: Proof. Proof using. case: t => [// | r0 t] /= _ /and4P[Hnnil0 Hrow0 _ _]. case: nrow => [| nrow]. - case: r0 Hnnil0 Hrow0 => [// | l0 [| l1 tl0]] _ H /= [_ <-] //=. exact: head_leq_last_row H. - case (invinstabnrow t nrow) => [tr lr]. have:= head_leq_invbumped lr Hnnil0 Hrow0. rewrite /invbumped. case (invbumprow lr r0) => [t0r l0r] /= H [_ <-]. by rewrite (set_head_default inh l0r Hnnil0). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab