take is redundant

[wilcoxjay]

The stdlib implements this as firstn

[palmskog]

stdlib gives very few lemmas for firstn, so some lemmas may be warranted to move to ListUtil.v. However, two of the proofs reduce to almost nothing when take is replaced with firstn:

Lemma take_length : forall n (xs : list A),
      length xs >= n ->
      length (firstn n xs) = n.
  Proof.
    intros.
    rewrite firstn_length.
    auto with arith.
  Qed.

  Lemma take_length_ge : forall n m (xs : list A),
      length (firstn n xs) >= m ->
      length xs >= m.
  Proof.
    intros.
    find_rewrite_lem firstn_length.
    eauto with arith.
  Qed.