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