proposition: Theorem exists_Qy : exists Q : {set {set 'I_(size y)}}, #|cover Q| = #|cover P| /\ Q \is a k.-supp[R, in_tuple y].
proof: Proof. Proof using HRabc HS Hposa Hposc Px x'. have eqxx' : x = x' by rewrite /x /x' -catA. pose eqsz := congr1 size eqxx'. have:= exists_Q_noboth => [] [Q [/= Hsupp Hcover Hnoboth]]. move HcastP : ((cast_set eqsz) @: Q) => Q'. exists (@NoSetContainingBoth.Q _ _ (u ++ [:: b]) v a c Q'); split. - rewrite -(eqP (@NoSetContainingBoth.size_cover_Q _ _ (u ++ [:: b]) v a c Q')). rewrite -HcastP cover_cast /cast_set /=. by rewrite card_imset; last exact: cast_ord_inj. - apply: NoSetContainingBoth.ksupp_Q. by rewrite -HcastP; apply: ksupp_cast. - move=> S1; rewrite -HcastP => /imsetP[S0 HS0 ->{S1}]. rewrite /cast_set /=. set x0 := (Swap.pos0 _ _ _ _); set x1 := (Swap.pos1 _ _ _ _). have:= Hnoboth S0 HS0. rewrite -(cast_ordKV eqsz x0) -(cast_ordKV eqsz x1). rewrite !(mem_imset _ _ (@cast_ord_inj _ _ _)). have -> : cast_ord (esym eqsz) x0 = posa. by apply: val_inj; rewrite /= size_cat /= addn1. suff -> : cast_ord (esym eqsz) x1 = posc by []. by apply: val_inj; rewrite /= size_cat /= addn1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene