proposition: Lemma disjoint_inj (sM : {set 'I_M}) (sN : {set 'I_N}) : [disjoint lsh @: sM & rsh @: sN].
proof: Proof. Proof using. rewrite /disjoint; apply/pred0P=> i /=. apply/negP => /andP[/imsetP[[l HlM] Hl -> {i}] /imsetP[[r HrN] Hr /eqP]]. by rewrite eq_lrshift. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype