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.
Last updated: Feb 01 2023 at 12:30 UTC