src/HOL/Inequalities.thy
changeset 61694 6571c78c9667
parent 61649 268d88ec9087
child 61762 d50b993b4fb9
     1.1 --- a/src/HOL/Inequalities.thy	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/HOL/Inequalities.thy	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -34,7 +34,7 @@
     1.4      by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum
     1.5            split: zdiff_int_split)
     1.6    thus ?thesis
     1.7 -    using int_int_eq by blast
     1.8 +    using of_nat_eq_iff by blast
     1.9  qed
    1.10  
    1.11  lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"