no goals
l r : List Char
it : Iterator
h : ValidFor l r it
x✝ : 0 ≤ List.length r
⊢ ValidFor (List.reverse (List.take 0 r) ++ l) (List.drop 0 r) (Iterator.nextn it 0)
simp [h, Iterator.nextn]
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ List.length r
⊢ ValidFor (List.reverse (List.take (n + 1) r) ++ l) (List.drop (n + 1) r) (Iterator.nextn (Iterator.next it) n)
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ List.length r
⊢ ValidFor (List.reverse (List.take (n + 1) r) ++ l) (List.drop (n + 1) r) (Iterator.nextn it (n + 1))
simp [h, Iterator.nextn]
l r✝ : List Char
it : Iterator
n : Nat
a : Char
r : List Char
h : ValidFor l (a :: r) it
hn : n + 1 ≤ List.length (a :: r)
⊢ ValidFor (List.reverse (List.take (n + 1) (a :: r)) ++ l) (List.drop (n + 1) (a :: r))
    (Iterator.nextn (Iterator.next it) n)
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ List.length r
⊢ ValidFor (List.reverse (List.take (n + 1) r) ++ l) (List.drop (n + 1) r) (Iterator.nextn (Iterator.next it) n)
have a::r := r
no goals
l r✝ : List Char
it : Iterator
n : Nat
a : Char
r : List Char
h : ValidFor l (a :: r) it
hn : n + 1 ≤ List.length (a :: r)
⊢ ValidFor (List.reverse (List.take (n + 1) (a :: r)) ++ l) (List.drop (n + 1) (a :: r))
    (Iterator.nextn (Iterator.next it) n)
simpa using h.next.nextn _ (Nat.le_of_succ_le_succ hn)