Theorem: dropEveryNth_eq_fun (ListPowersProblem.lean)

State before:
n : ℕ
α✝ : Type u_1
σ : Stream' α✝
⊢ dropEveryNth (n + 1) σ = fun i => σ (i + i / n)
Tactic:
rw [dropEveryNth, fun_to_corec fun i => σ (i + i/n)]
State after:
n : ℕ
α✝ : Type u_1
σ : Stream' α✝
⊢ corec
      (fun x =>
        match x with
        | (σ, snd) => head σ)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), n + 1 - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, n + 1 - 2) =
    corec (fun i => σ (i + i / n)) (fun x => x + 1) 0