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: Jun 14 2024 at 19:02 UTC