Sum of the first n naturals

import Mathlib

theorem gauss_sum (n : Nat) : 2 * (∑ i ∈ Finset.range (n + 1), i) = n * (n + 1) :=by
  rw [mul_comm 2]
  rw [Finset.sum_range_id_mul_two (n + 1)]
  rw [Nat.add_sub_cancel]
  ring