I was surprised not to find (sic) the following two limit cases among the other
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
Indeed, that looks worth a pull request to add them.
Last updated: Nov 29 2023 at 21:01 UTC