import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Tactic.Ring

ttheorem gauss_sum_identity_100 : 2 * Finset.sum (Finset.range (100 + 1)) id = 100 * (100 + 1) := by
  rw [Finset.sum_range_id]
  ring_nf
  rfl