I was surprised not to find (sic) the following two limit cases among the other `find`

lemmas:

```
Lemma findT T (s : seq T) : find xpredT s = 0.
Proof. by elim: s. Qed.
Lemma find0 T (s : seq T) : find xpred0 s = size s.
Proof. by []. Qed.
```

Have I missed something? If not, shouldn't they be added (or at least the first one) to the `seq.v`

library?

Indeed, that looks worth a pull request to add them.

Last updated: Jul 24 2024 at 12:02 UTC