proposition: Lemma uniq_subseq_size (T: eqType) (l l': seq T) : all (fun x => x \in l) l' -> uniq l' -> (size l' <= size l)%N.
proof: Proof. elim: l' l=>// a l' IHl' l /andP[al /allP l'l] /andP [al' l'uniq]. move:(al)=>/size_rem/(f_equal S). rewrite prednK; last by case: l l'l al. move=><-; rewrite ltnS; apply IHl'=>//. apply/allP=>b bl'; move:(bl')=>/l'l bl. apply/negPn/negP=>/count_memPn brem. move:al=>/perm_to_rem /allP /(_ b). rewrite mem_cat bl/= =>/(_ Logic.eq_refl); rewrite brem. case ab: (a == b); first by move=>_; move: al'=>/negP; apply; move: ab=>/eqP->. by move=>/=/eqP/count_memPn/negP; apply. Qed.
imports: mathcomp(all_ssreflect ssrnum zmodp order constructive_ereal) preliminaries