proposition: Lemma lshift_in_rshift_recF i (s : {set 'I_(size t0)}) : lsh_rec i \in [set rsh_rec x | x in s] = false.
proof: Proof. Proof using. by apply/negP => /imsetP[j _ /eqP]; rewrite lrshift_recF. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype