proposition: Lemma ksuppCol_inj_plact2i : v2 \in plact2i v1 -> ksupp_inj >%O >%O k (u ++ v1 ++ w) (u ++ v2 ++ w).
proof: Proof. Proof using. move/plact2iP => [a] [b] [c] [Hord -> ->]. have Hyp := SetContainingBothLeft.RabcGtnX Hord. have Hbca : ((u ++ [:: b]) ++ [:: c; a] ++ w) = (u ++ [:: b; c; a] ++ w) by rewrite -catA. have Hbac : ((u ++ [:: b]) ++ [:: a; c] ++ w) = (u ++ [:: b; a; c] ++ w) by rewrite -catA. rewrite -Hbca -Hbac /ksupp_inj => P Hsupp. pose posa := (Swap.pos0 (u ++ [:: b]) w c a). pose posc := (Swap.pos1 (u ++ [:: b]) w c a). case (boolP [exists S, [&& S \in P, posa \in S & posc \in S] ]). - move/existsP => [S /and3P[HSin HSa HSc]]. move HcastP : ((cast_set (congr1 size Hbca)) @: P) => P'. have Hsupp' : P' \is a k.-supp[>%O, in_tuple (u ++ [:: b; c; a] ++ w)] by rewrite -HcastP; exact: ksupp_cast. move HcastS : (cast_set (congr1 size Hbca) S) => S'. have HS'in : S' \in P' by rewrite -HcastP -HcastS; apply: imset_f. set pos1 := Swap.pos1 u (a :: w) b c. have {posa HSa} Hpos1 : pos1 \in S'. rewrite -(cast_ordKV (congr1 size Hbca) pos1) -HcastS /cast_set /=. apply: imset_f. suff -> /= : cast_ord (esym (congr1 size Hbca)) pos1 = posa by []. by apply: val_inj; rewrite /= size_cat /= addn1. set pos2 := Ordinal (SetContainingBothLeft.u2lt u w c b a). have {posc HSc} Hpos2 : pos2 \in S'. rewrite -(cast_ordKV (congr1 size Hbca) pos2) -HcastS /cast_set /=. apply: imset_f. suff -> /= : cast_ord (esym (congr1 size Hbca)) pos2 = posc by []. by apply: val_inj; rewrite /= size_cat /= addn1. have {pos1 pos2 Hyp Hsupp' S' HcastS HS'in Hpos1 Hpos2} [Q [Hcover HsuppQ]] := SetContainingBothLeft.exists_Qy Hyp Hsupp' HS'in Hpos1 Hpos2. exists Q; apply/andP; split; last exact HsuppQ. by rewrite Hcover -HcastP -size_cover_inj //=; exact: cast_ord_inj. - rewrite negb_exists => /forallP Hall. exists (NoSetContainingBoth.Q P); rewrite NoSetContainingBoth.size_cover_Q /=. apply: NoSetContainingBoth.ksupp_Q; first exact Hsupp. by move=> S HS; have:= Hall S; rewrite HS /= => /negbTE ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene