proposition: Lemma take_spec : forall n l, 0 <= n <= length l -> exists l', length (take n l) = n /\ l = (take n l) ++ 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)