proposition: Lemma rank_le x (s : seq V) : uniq s -> rank x s <= infty.
proof: Proof. move=> s_uniq; rewrite rankE; case: ifP => // x_s. by rewrite (leq_trans (index_size _ _)) ?size_rev -?(card_uniqP _) // max_card. Qed.
imports: mathcomp(all_ssreflect) extra