α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (even s) (succ n) = nth s (succ (succ (2 * n)))
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (even s) (succ n) = nth s (2 * succ n)
change nth (even s) (succ n) = nth s (succ (succ (2 * n)))
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (tail (tail s)) (2 * n) = nth (tail s) (2 * n + 1)
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (even s) (succ n) = nth s (succ (succ (2 * n)))
rw [nth_succ, nth_succ, tail_even, nth_even n]
no goals
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (tail (tail s)) (2 * n) = nth (tail s) (2 * n + 1)
rfl