Proving laws of take and drop functions using structural induction on lists
You can prove the second law by induction on n:


Base case:


drop m (drop 0 xs) = drop m xs (definition of drop, base case)

= drop (m + 0) xs (since m + 0 = m)


Inductive step:


We have to consider two cases: when the input list is empty, and when it's not empty. When it's empty, we have

drop m (drop n []) = drop m [] = [] = drop (m + n) [] (definition of drop, base case)

When the input list is not empty, we have

drop (m + n) (x:xs) = drop (m + n - 1) xs (definition of drop, inductive case)

= drop m (drop (n - 1) xs) (inductive hypothesis)

= drop m (drop n (x:xs)) (definition of drop, inductive case)

I imagine that the first law is not much more difficult. Try to prove it by induction on n, and if it doesn't work, try induction on m. One of them will probably work.