proposition: Lemma std_rcons_shiftinv t tn : is_std (rcons t tn) -> std t = map (shiftinv_pos tn) t.
proof: Proof. move=> H; apply/eqP/stdP; constructor. - rewrite /is_std size_map perm_sym. apply: perm_size_uniq. + exact: iota_uniq. + move=> i; move: H; rewrite /is_std => /perm_mem Hperm. case (ltnP i tn) => Hi. * have {2}-> : i = shiftinv_pos tn i by rewrite /shiftinv_pos Hi. move=> Hiota; apply: map_f; have:= Hperm i; move: Hiota. rewrite !mem_iota /= !add0n size_rcons ltnS => /ltnW ->. by rewrite mem_rcons inE (ltn_eqF Hi) /= => ->. * have {2}-> : i = shiftinv_pos tn i.+1. by rewrite /shiftinv_pos ltnNge (leq_trans Hi (leqnSn _)). move=> Hiota; apply: map_f; have:= Hperm i.+1; move: Hiota. rewrite !mem_iota /= !add0n size_rcons ltnS => ->. rewrite mem_rcons inE. by move: Hi; rewrite -ltnS => /ltn_eqF; rewrite eq_sym => -> /= ->. + by rewrite size_map size_iota. - apply/eq_invP; split; first by rewrite size_map. move=> i j /andP[Hij Hj]. rewrite (nth_map inh); last exact (leq_ltn_trans Hij Hj). rewrite (nth_map inh); last exact Hj. rewrite !leEnat. apply/idP/idP; first exact: shiftinv_pos_homo. apply: contraLR. rewrite -!ltnNge !ltn_neqAle => /andP[Hneq /shiftinv_pos_homo ->]. rewrite andbT. have:= std_uniq H; rewrite rcons_uniq => /andP[Htn Huniqt]. move: Hneq; set xi := nth _ _ i; set xj := nth _ _ j. rewrite /shiftinv_pos. case (ltnP xi tn) => Hxi; case (ltnP xj tn) => Hxj. + by apply. + apply: contra => /eqP H1; move: Hxj Hxi; rewrite -{i xi Hij}H1 => H1 H2. exfalso; have Hneq : xj != tn. by move: Htn; apply: contra => /eqP <-; rewrite /xj mem_nth. move: H2; have {H1 Hneq} : tn < xj by rewrite ltn_neqAle eq_sym Hneq H1. case: xj => [// | x] /=. rewrite ltnS => H1 H2; have:= leq_ltn_trans H1 H2. by rewrite ltnn. + apply: contra => /eqP H1; move: Hxj Hxi. have {Hij Hj} Hi := leq_ltn_trans Hij Hj; rewrite {j xj}H1 => H1 H2. exfalso. have Hneq : xi != tn. by move: Htn; apply: contra => /eqP <-; rewrite /xi mem_nth. have {H2 Hneq} : tn < xi by rewrite ltn_neqAle eq_sym Hneq H2. case: xi H1 => [// | x] /=. rewrite ltnS => H1 H2; have := leq_ltn_trans H2 H1. by rewrite ltnn. + apply: contra => /eqP H1. have Hi := leq_ltn_trans Hij Hj. have {Hxi} : tn < xi. rewrite ltn_neqAle Hxi andbT. by move: Htn; apply: contra => /eqP ->; rewrite /xi mem_nth. have {Hxj} : tn < xj. rewrite ltn_neqAle Hxj andbT. by move: Htn; apply: contra => /eqP ->; rewrite /xj mem_nth. case: xi H1 => [// | xi] /=. by case: xj => [// | xj] /= ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv