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: Jun 17 2024 at 22:01 UTC