I have function whose output is a list and its length is some positive natural number which is less or equal than (S m). I am selecting n natural numbers from above output list by using firstn function. Please guide me how i should write in terms of lemma statement and how to relate length n of firstn function with Sm.

You may look at some related lemmas in the `List`

library with the command `Search firstn length`

.

Last updated: Oct 03 2023 at 02:34 UTC