proposition: Lemma rank_small x s : uniq s -> (rank x s < size s) = (x \in s).
proof: Proof. move=> s_uniq; rewrite rankE; case: (boolP (x \in s)) => [xNs|_]. by rewrite -size_rev index_mem mem_rev. apply: negbTE; rewrite -ltnNge ltnS cardE uniq_leq_size //. by move=> y; rewrite mem_enum. Qed.
imports: mathcomp(all_ssreflect) extra