have r1 : Finset.range N = Finset.range ⌈ε * N⌉₊ ∪ Finset.Ico ⌈ε * N⌉₊ N := by
  rw [Finset.range_eq_Ico] ; symm ; apply Finset.Ico_union_Ico_eq_Ico (by simp)
  simp ; convert_to ε * ↑N ≤ 1 * ↑N ; ring ; gcongr
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N