src/HOL/Inequalities.thy
changeset 60150 bd773c47ad0b
parent 59720 f893472fff31
child 60167 9a97407488cd
     1.1 --- a/src/HOL/Inequalities.thy	Tue Apr 28 16:23:05 2015 +0100
     1.2 +++ b/src/HOL/Inequalities.thy	Tue Apr 28 16:23:38 2015 +0100
     1.3 @@ -7,14 +7,6 @@
     1.4    imports Real_Vector_Spaces
     1.5  begin
     1.6  
     1.7 -lemma setsum_triangle_reindex:
     1.8 -  fixes n :: nat
     1.9 -  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
    1.10 -  apply (simp add: setsum.Sigma)
    1.11 -  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
    1.12 -  apply auto
    1.13 -  done
    1.14 -
    1.15  lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow>
    1.16    setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)"
    1.17  using gauss_sum[where n=n and 'a = 'a,symmetric] by auto