proposition: Lemma take_app_drop_spec : forall n l f r, f = take n l -> r = drop n l -> (0 <= n <= length l -> l = f ++ r /\ length f = n /\ length r = length l - n) /\ (n <= 0 -> f = nil /\ r = l).
proof: Proof. Proof using. introv ? ?. split. { intros (? & Hn). unfold take, drop, length in *. forwards~ (? & ? & Hlenrest): @LibList.take_app_drop_spec (to_nat n) l f r. } { intros. rewrites~ take_neg in *. rewrites~ drop_neg in *. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)