proposition: Lemma linvseqK s0 s t tn : invseq (s0 :: s) (rcons t tn) -> linvseq (rembig (s0 :: s)) (std t).
proof: Proof. move=> Hinv. rewrite (std_rcons_shiftinv (invseq_is_std (invseq_sym Hinv))). have := Hinv; rewrite /invseq => /andP[/linvseqP Hst /linvseqP Hts]. apply/linvseqP => i Hi. rewrite (set_nth_default inh _ Hi) -nth_rembig. rewrite (nth_map (size (s0 :: s))); first last. set si := shift_pos _ _; have Hsipos : si != posbig (s0 :: s). rewrite /si /shift_pos; case: (ltnP i (posbig (s0 :: s))). + by move /ltn_eqF ->. + by rewrite -ltnS => /gtn_eqF ->. have Hsi : si < (size (s0 :: s)). rewrite /si /shift_pos; case: (ltnP i (posbig (s0 :: s))) => H. + by apply: (ltn_trans Hi); rewrite size_rembig /=. + by apply: (leq_trans Hi); rewrite size_rembig /=. apply: (leq_trans (nth_std_pos _ (invseq_is_std Hinv) Hsi Hsipos)). by move: Hinv => /size_invseq /=; rewrite size_rcons => /succn_inj ->. rewrite (posbig_invseq Hinv). have Hpos : shift_pos tn i < size (s0 :: s). move: Hi; rewrite /shift_pos size_rembig /=. by case (i < tn); first by move/leq_trans; apply. rewrite (set_nth_default (size (rcons t tn)) inh Hpos). move: (Hst _ Hpos); rewrite nth_rcons. rewrite (_ : nth _ _ _ < size t); first by move ->; rewrite shift_posK. have -> : size t = (size (s0 :: s)).-1 by rewrite (size_invseq Hinv) size_rcons. apply: (nth_std_pos (size (rcons t tn)) (invseq_is_std Hinv) Hpos). rewrite (posbig_invseq Hinv) /shift_pos. case (ltnP i tn); first by move /ltn_eqF ->. by rewrite -ltnS => /gtn_eqF ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv