case h.h.h
s n : Nat
step : optParam Nat 1
⊢ range' s n step = range'TR s n step
⊢ range' = range'TR
funext s n step
case h.h.h
s n : Nat
step : optParam Nat 1
⊢ range' s n step = range'TR s n step
case h.h.h
s n : Nat
step : optParam Nat 1
⊢ range' s n step = range'TR s n step
let rec go (s) : ∀ n m,
  range'TR.go step n (s + step * n) (range' (s + step * n) m step) = range' s (n + m) step
| 0, m => by simp [range'TR.go]
| n+1, m => by
  simp [range'TR.go]
  rw [Nat.mul_succ, ← Nat.add_assoc, Nat.add_sub_cancel, Nat.add_right_comm n]
  exact go s n (m + 1)
no goals
case h.h.h
s n : Nat
step : optParam Nat 1
⊢ range' s n step = range'TR s n step
exact (go s n 0).symm
no goals
s✝ n : Nat
step : optParam Nat 1
s m : Nat
⊢ range'TR.go step 0 (s + step * 0) (range' (s + step * 0) m step) = range' s (0 + m) step
simp [range'TR.go]
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step n (s + step * (n + 1) - step) ((s + step * (n + 1) - step) :: range' (s + step * (n + 1)) m step) =
    range' s (n + 1 + m) step
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step (n + 1) (s + step * (n + 1)) (range' (s + step * (n + 1)) m step) = range' s (n + 1 + m) step
simp [range'TR.go]
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step n (s + step * n) ((s + step * n) :: range' (s + step * n + step) m step) = range' s (n + m + 1) step
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step n (s + step * (n + 1) - step) ((s + step * (n + 1) - step) :: range' (s + step * (n + 1)) m step) =
    range' s (n + 1 + m) step
rw [Nat.mul_succ, ← Nat.add_assoc, Nat.add_sub_cancel, Nat.add_right_comm n]
no goals
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step n (s + step * n) ((s + step * n) :: range' (s + step * n + step) m step) = range' s (n + m + 1) step
exact go s n (m + 1)