proposition: Lemma ksuppRow_inj_plact1i : v2 \in plact1i v1 -> ksupp_inj <=%O <=%O k (u ++ v1 ++ w) (u ++ v2 ++ w).
proof: Proof. Proof using. move/plact1iP => [a] [b] [c] [Hord -> ->]. rewrite /ksupp_inj => S1 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 S1, posa \in S & posc \in S] ]). - move/existsP => [S /and3P[HSin HSa HSb]]. exfalso; move: Hsupp => /and3P[_ _ /forallP Hall]. move/(_ S): Hall; rewrite HSin /=. move/(sorted_extract_cond le_trans [set posa; posc]). have -> : S :&: [set posa; posc] = [set posa; posc]. apply/setP/subset_eqP/andP. split; apply/subsetP=> i; first by rewrite inE => /andP[]. rewrite !inE => /orP[] /eqP ->; rewrite eq_refl /=; first by rewrite HSa. by rewrite HSb orbT. have /extract2 -> : posa < posc by []. rewrite !(tnth_nth b) /= andbT. elim u => [| u0 u'] //=. move: Hord => /andP[/le_lt_trans /[apply]]. by rewrite leNgt => ->. - rewrite negb_exists => /forallP Hall. exists (NoSetContainingBoth.Q S1); 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