sara lee (Jul 08 2022 at 04:22): sara lee (Jul 08 2022 at 04:22):I have taken two lemmas from library . Want to see their proof in the library but i did not find it, where I will look for them?
Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n.
Lemma firstn_length_le: forall l:list A, forall n:nat, n <= length l -> length (firstn n l) = n.
Use search engine. Or look into the Coq git repo where the stdlib is defined.
For your specific lemmas, they're here.
sara lee (Jul 08 2022 at 07:37):Ok,thank you.
Last updated: Oct 13 2024 at 01:02 UTC