# HG changeset patch # User paulson # Date 1600412539 -3600 # Node ID 71a8935eb5da612f37ee607cb0f630661b587005 # Parent 121b838a0ba891a93d676d1877ba68bf0b61a57f removal of needless premises diff -r 121b838a0ba8 -r 71a8935eb5da src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Thu Sep 17 18:48:37 2020 +0100 +++ b/src/HOL/Set_Interval.thy Fri Sep 18 08:02:19 2020 +0100 @@ -2171,7 +2171,7 @@ subsubsection \The formula for geometric sums\ lemma sum_power2: "(\i=0.. 1" @@ -2205,31 +2205,31 @@ corollary power_diff_sumr2: \ \\COMPLEX_POLYFUN\ in HOL Light\ fixes x :: "'a::{comm_ring,monoid_mult}" - shows "x^n - y^n = (x - y) * (\ii 0 \ x^n - 1 = (x - 1) * (\ii 0 \ 1 - x^n = (1 - x) * (\ii 0 \ 1 - x^n = (1 - x) * (\iii\n. x^i) = 1 - x^Suc n" - by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost) + by (simp only: one_diff_power_eq lessThan_Suc_atMost) lemma sum_power_shift: fixes x :: "'a::{comm_ring,monoid_mult}"