`take_app_ge` has unneeded side-condition

Lemma take_app_ge l k n :
  length l ≤ n → take n (l ++ k) = l ++ take (n - length l) k.

length l ≤ n is not needed.

In fact, the stdlib has firstn_app which exactly the above std++ lemma without side-condition.