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