Stream: Coq users

Topic: Total elements

view this post on Zulip 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.

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC