proposition: Lemma revsetK {n} : involutive (@revset n).
proof: Proof. Proof using. rewrite /revset => s. rewrite -imset_comp -setP => i /=. apply/imsetP/idP => [[x /= Hx ->] | Hi]. - by rewrite rev_ordK. - by exists i => //=; rewrite rev_ordK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype