proposition: Theorem Sch_exists w i : i < size (Sch w) -> exists s : seq T, (last inh s == nth inh (Sch w) i) && subseqrow_n s w i.+1.
proof: Proof. Proof using. rewrite /subseqrow_n. elim/last_ind: w i => [// | w wn IHw] i. rewrite Sch_rcons {2}/ins. case: (i =P (inspos (Sch w) wn)) => [| /eqP Hineq Hileq]. - case: i => [<- | i Hieq ] _. + by exists [:: wn] => /=; case (Sch w) => /= [|_ _]; rewrite -cats1 suffix_subseq; apply/and3P; repeat split. + have:= inspos_leq_size (Sch w) wn; rewrite -Hieq. move=> {}/IHw [s] /and4P[/eqP Hlast Hsubs /eqP Hsz Hrow]. exists (rcons s wn); apply/and4P; repeat split. + by rewrite last_rcons nth_set_nth_any eq_refl. + by rewrite -subseq_rcons_eq. + by rewrite size_rcons Hsz. + apply: (is_row_rcons Hrow). have Hany : (size s).-1 < size s by rewrite Hsz. rewrite -nth_last (set_nth_default inh wn Hany) {Hany} nth_last Hlast. have:= inspos_leq_size (Sch w) wn; rewrite -Hieq => Hany. rewrite (set_nth_default wn inh Hany). by apply: nth_lt_inspos; rewrite -Hieq ltnSn. - have Hi : (i < size (Sch w)); have HrowSch := is_row_Sch w. move: Hineq Hileq; case (boolP (bump (Sch w) wn )) => Hcase. + by rewrite (bump_size_ins HrowSch Hcase). + rewrite (nbump_inspos_eq_size HrowSch Hcase) (nbump_size_ins HrowSch Hcase). by rewrite ltnS ltn_neqAle => -> ->. case (IHw _ Hi) => {IHw} s => /and4P[/eqP Hlast Hsubs /eqP Hsz Hrow]. exists s; apply/and4P; repeat split. + by rewrite /ins in Hileq; rewrite nth_set_nth_any (negbTE Hineq) Hi Hlast. + apply: (subseq_trans Hsubs); exact: subseq_rcons. + by rewrite Hsz. + exact Hrow. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab