proposition: Lemma list_eq_take_app_drop : forall n l, n <= length l -> take n l ++ drop n l = l.
proof: Proof. Proof using. introv H. tests: (0 <= n). { forwards*: take_app_drop_spec n l. } { rewrite~ take_neg. rewrite~ drop_neg. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)