proposition: Lemma pos01F : (pos0 == pos1) = false.
proof: Proof. Proof using. by rewrite /eq_op /= ltn_eqF. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene