proposition: Lemma drop_spec : forall n l, 0 <= n <= length l -> exists l', length l' = n /\ l = l' ++ (drop n l).
proof: Proof. Proof using. introv E. forwards* (E1&_): take_app_drop_spec. forwards*: E1. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)