proposition: Lemma ord0_in_map_liftF n (l : seq 'I_n) : ord0 \in [seq lift ord0 i | i <- l] = false.
proof: Proof. elim: l => [| l0 l] /=; first by rewrite in_nil. by rewrite in_cons; have:= neq_lift ord0 l0; rewrite eq_sym => /negbTE ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast