proposition: Lemma ksupp_cast R (w1 w2 : seq T) (H : w1 = w2) k Q : Q \is a k.-supp[R, in_tuple w1] -> (cast_set (congr1 size H)) @: Q \is a k.-supp[R, in_tuple w2].
proof: Proof. subst w1; rewrite /=. suff /eq_imset -> : cast_set (congr1 size (erefl w2)) =1 id by rewrite imset_id. move=> U; rewrite /cast_set /=. suff /eq_imset -> : cast_ord (congr1 size (erefl w2)) =1 id by rewrite imset_id. by move=> i; rewrite cast_ord_id. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype