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