Lean: reindex ∑ k ∈ Icc 1 n, f (n - k) to ∑ j ∈ range n, f j with sum_bij'

For convolution-type recursions you often need ∑_{k ∈ Icc 1 n} c k * u (n - k) = ∑_{j < n} u j (when c is constant). rw-based reflections (sum_range_reflect, range_eq_Ico, sum_eq_sum_Ico_succ_bot, then show Ico (0+1) (n+1) = Icc 1 n from rfl) work but are fiddly. A robust alternative: refine sum_bij' (fun k _ ↦ n - k) (fun j _ ↦ n - j) (fun k hk ↦ ?_) (fun j hj ↦ ?_) (fun k hk ↦ ?_) (fun j hj ↦ ?_) (fun k hk ↦ ?_). Close the four membership/inverse goals with simp only [mem_Icc, mem_range] at *; omega, and the last goal by rewriting the summand. Combined with strong induction (Nat.strong_induction_on), this turns 'the recursion determines the sequence' into a ~25-line uniqueness proof.