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