proposition: Lemma take_app_l : forall n l l', (n <= length l) -> take n (l ++ l') = take n l.
proof: Proof. Proof using. intros. tests: (0 <= n). { unfold take, length in *. applys~ LibList.take_app_l. } { rewrite !take_neg; auto; math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)