proposition: Lemma drop_app_r : forall n l l', (n >= length l) -> drop n (l ++ l') = drop (n - length l) l'.
proof: Proof. Proof using. intros. unfold drop, length in *. rew_to_nat_nonneg~. apply LibList.drop_app_r. rewrites~ to_nat_ge_nat_ge. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)