proposition: Lemma take_succ : forall x l n, 0 <= n -> take (n+1) (x::l) = x :: (take n l).
proof: Proof. Proof using. intros. unfold take. rew_to_nat_nonneg~. rewrite Nat.add_1_r. apply LibList.take_succ. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)