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