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