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: Oct 13 2024 at 01:02 UTC