proposition: Lemma last_big_append_nth t b lb : (forall j : nat, j < lb -> (last b (nth [::] t j) < b)%O) -> last_big (append_nth t b lb) b = lb.
proof: Proof. Proof using. elim: t lb =>[| t0 t IHt] /=. - case => [_| lb Hj] /=; first by rewrite eq_refl. by exfalso; have:= Hj 0 (ltn0Sn _); rewrite ltxx. - case => [_| lb Hj] /=; first by rewrite last_rcons eq_refl. rewrite (lt_eqF (Hj 0 (ltn0Sn _))). by rewrite -/(append_nth _ _ _) IHt // => k Hk; exact: (Hj k.+1 Hk). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau