Add new proof take-all to Data.List.Properties (#1983)

Author: Sofia-Insa

CHANGELOG.md

@@ -2152,7 +2152,8 @@ Other minor changes
 
   length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
   length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
- 
+  
+  take-all : n ≥ length xs → take n xs ≡ xs     
   take-[] : ∀ m → take  m [] ≡ []
   drop-[] : ∀ m → drop  m [] ≡ []
   ```

src/Data/List/Properties.agda

@@ -759,6 +759,12 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
+-- If you take at least as many elements from a list as it has, you get the whole list.
+take-all :(n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs
+take-all zero [] _ = refl
+take-all (suc _) [] _ = refl
+take-all (suc n) (x ∷ xs) (s≤s pf) = cong (x ∷_) (take-all n xs pf)
+
 -- Taking from an empty list does nothing.
 take-[] : ∀ m → take {A = A} m [] ≡ []
 take-[] zero = refl