proposition: Lemma index_le (A:finType) (x:A): index x < length (elem A).
proof: Proof. unfold index. assert (H:x el elem A) by apply elem_spec. revert H. generalize (elem A). intros l H. induction l;cbn;[|decide _]. - easy. - lia. - destruct H. congruence. apply IHl in H. lia. Qed.