proposition: Lemma TSneq : T != S.
proof: Proof. Proof using HRabc HS HT Hposa Hposb Px. apply/eqP=> Heq; subst T. have:= Hba HRabc; suff -> : R b a by []. move: Px => /and3P[_ _ /forallP Hall]. move/(_ S): Hall; rewrite HS. move/(sorted_extract_cond (Rtrans HRabc) [set posb; posa]). have -> : S :&: [set posb; posa] = [set posb; posa]. apply/setP/subset_eqP/andP. split; apply/subsetP=> i; first by rewrite inE => /andP[]. rewrite !inE => /orP[] /eqP ->; rewrite eq_refl /=; first by rewrite Hposb. by rewrite Hposa orbT. have /extract2 -> : posb < posa by []. by rewrite Swap.tnth_pos0 Swap.tnth_pos1 /= andbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene