proposition: Lemma invbump_dom r0 t tin l nrow : t != [::] -> is_tableau t -> invinstabnrow t nrow = (tin, l) -> r0 != [::] -> dominate (head [::] t) r0 -> invbump l r0.
proof: Proof. Proof using. rewrite /invbump => Htnnil Ht /(invbump_geq_head Htnnil Ht). case: t Htnnil Ht => [// | r1 t] /= _ /and4P[Hnnil1 _ _ _]. case: r1 Hnnil1 => [// | l1 r1 ] /= _ Hl1. case: r0 => [// | l0 r0 ] /= _ /dominateP[_ /(_ 0 (ltn0Sn _))] => /= Hl0. exact: lt_le_trans Hl0 Hl1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab