src/HOL/Library/Uprod.thy
changeset 66936 cf8d8fc23891
parent 66563 87b9eb69d5ba
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Library/Uprod.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Library/Uprod.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -206,13 +206,13 @@
     1.4      apply(rule card_image)
     1.5      using bij[THEN bij_betw_imp_inj_on]
     1.6      by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans)
     1.7 -  also have "\<dots> = sum (\<lambda>n. n + 1) {0..<?A}"
     1.8 -    by(subst card_SigmaI) simp_all
     1.9 -  also have "\<dots> = 2 * sum of_nat {1..?A} div 2"
    1.10 -    using sum.reindex[where g="of_nat :: nat \<Rightarrow> nat" and h="\<lambda>x. x + 1" and A="{0..<?A}", symmetric] True
    1.11 -    by(simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
    1.12 +  also have "\<dots> = sum Suc {0..<?A}"
    1.13 +    by (subst card_SigmaI) simp_all
    1.14 +  also have "\<dots> = sum of_nat {Suc 0..?A}"
    1.15 +    using sum.atLeast_lessThan_reindex [symmetric, of Suc 0 ?A id]
    1.16 +    by (simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
    1.17    also have "\<dots> = ?A * (?A + 1) div 2"
    1.18 -    by(subst gauss_sum) simp
    1.19 +    using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp
    1.20    finally show ?thesis .
    1.21  qed simp
    1.22