proposition: Theorem Sch_leq_last w s si: subseqrow (rcons s si) w -> size s < size (Sch w) /\ (nth inh (Sch w) (size s) <= si)%O.
proof: Proof. Proof using. rewrite /subseqrow => /andP[]. elim/last_ind: w s si => [| w wn IHw] s si; first by rewrite subseq0 rcons_nilF. rewrite Sch_rcons /=; have HSch := is_row_Sch w. case: (si =P wn) => [-> {si} | /eqP Hsiwn Hsubs Hrow]. - rewrite -subseq_rcons_eq. case/lastP: s => [ _ _ {IHw} | s si Hsubs Hrow]. + split; first by rewrite size_ins_non_0. have:= size_ins_non_0 (Sch w) wn => Hany. rewrite -[size [::]]/(0) (set_nth_default wn inh Hany) nth0. apply: ins_head_lt. exact: is_row_Sch. move/(_ _ _ Hsubs (is_row_rconsK Hrow)): IHw => [Hszlt Hlt]. have:= is_row_last Hrow; rewrite last_rcons => Hsiwn. case (boolP (bump (Sch w) wn )) => [Hbump | Hnbump]. + have Hszpos: (size s < inspos (Sch w) wn). apply: (lt_inspos_nth (is_row_Sch w) Hszlt). by rewrite (set_nth_default inh wn Hszlt); exact: (le_trans Hlt Hsiwn). rewrite size_rcons (bump_size_ins HSch Hbump); split. * exact: (leq_ltn_trans Hszpos (bump_inspos_lt_size HSch Hbump)). * rewrite {2}(_: wn = nth inh (ins (Sch w) wn) (inspos (Sch w) wn)); last by rewrite /ins nth_set_nth_any eq_refl. apply (is_rowP _ _ (is_row_ins HSch wn)). by rewrite Hszpos size_set_nth leq_max ltnSn. + rewrite (nbump_ins_rconsE HSch Hnbump) !size_rcons nth_rcons. split; first by []. case: (leqP (size s).+2 (size (Sch w))) => Hsz. * apply: (@le_trans _ T (last inh (Sch w)) _ wn); first last. rewrite -nth_last (set_nth_default wn inh); first by rewrite nth_last -notbump. by rewrite -{2}(ltn_predK Hsz). rewrite -(nth_last inh). apply: (is_rowP _ _ HSch). have:= Hsz; rewrite -{1}(ltn_predK Hsz) ltnS => -> /=. by rewrite -{2}(ltn_predK Hsz); exact: ltnSn. * case eqP => [// | Habs]. exfalso; rewrite ltnS in Hsz; move: Habs => /eqP. by rewrite eqn_leq Hsz Hszlt. - move: Hsubs; rewrite subseq_rcons_neq // => /(IHw _ _)/(_ Hrow) {Hsiwn Hrow}. move=> [Hsize Hleq]; split. * by apply: (leq_trans Hsize); exact: size_ins_inf. * rewrite (set_nth_default wn inh Hsize) in Hleq. rewrite (set_nth_default wn inh (leq_trans Hsize (size_ins_inf HSch wn))). exact: (le_trans (ins_leq HSch wn Hsize) Hleq). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab