proposition: Lemma rank_lt x (s : seq V) : uniq s -> (rank x s < infty) = (x \in s).
proof: Proof. rewrite rankE; case: ifPn; rewrite ?ltnn // => x_s s_uniq. rewrite (@leq_trans (size (rev s))) ?index_mem ?mem_rev ?size_rev //. by rewrite -?(card_uniqP _) // max_card. Qed.
imports: mathcomp(all_ssreflect) extra