proposition: Lemma last_bigP t b i : is_tableau t -> allLeq (to_word t) b -> reflect (last b (nth [::] t i) = b /\ forall j, j < i -> (last b (nth [::] t j) < b)%O) (i == last_big t b).
proof: Proof. Proof using. move=> Htab Hmax; apply: (iffP eqP) => [-> | []]; first split. - elim: t Htab {Hmax} => [// | t0 t IHt] /= /and4P[_ _ _ Htab]. by case eqP => [// | _]; apply: IHt. - elim: t Htab Hmax => [// | t0 t IHt] /= /and4P[Hnnil _ _ Htab] Hmax. case eqP => [// | /eqP H]. case=> [/= _ | j]. + rewrite lt_neqAle {}H /=; move/allLeq_to_word_hd : Hmax. by case/lastP: t0 Hnnil => [// | t0 tn] _; rewrite last_rcons => /allLeq_last. + by rewrite /=; apply IHt; last exact: (allLeq_to_word_tl Hmax). - elim: t i Htab Hmax => [/= i _ _| t0 t IHt]. + by case: i => [// | i] /= _ /(_ 0 (ltn0Sn _)) /=; rewrite ltxx. + case=> [/= _ _ -> _| i]; first by rewrite eq_refl. move=> /= /and4P[_ _ _ Htab] Hmax Hlast Hj. have:= Hj 0 (ltn0Sn _) => /= /lt_eqF ->. rewrite (IHt _ Htab (allLeq_to_word_tl Hmax) Hlast) //. by move=> j; apply: (Hj j.+1). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau