theory Intro_Example
  imports Main
begin

lemma "sum (\<lambda>i. i :: nat) {0..n} = n * (n + 1) div 2"
  sledgehammer (del: gauss_sum_nat gauss_sum gauss_sum_nat gauss_sum_from_Suc_0
      Sum_Icc_nat Sum_Ico_nat)
  sorry

end
