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.

Ok,thank you.

Last updated: Oct 05 2023 at 02:01 UTC