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