proposition: Lemma card_seq (s : seq T) : #|[set i in s]| <= size s.
proof: Proof. Proof using. elim: s => [// | s0 s IHs]. - suff -> : [set i | i \in [::]] = set0 :> {set T} by rewrite cards0. by apply setP => i /=; rewrite inE. - rewrite set_cons cardsU1 /= -add1n. by apply: leq_add; first by case: (s0 \notin [set i in s]). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast