sara lee (Jul 16 2022 at 17:29): sara lee (Jul 16 2022 at 17:29):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.
Pierre Castéran (Jul 17 2022 at 19:35):You may look at some related lemmas in the List library with the command Search firstn length.
Last updated: Oct 13 2024 at 01:02 UTC