[STATEMENT]
lemma sum_of_powers_int: "(x - 1::int) * (\<Sum>i=0..n . x^i) = x ^ Suc n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x - 1) * sum ((^) x) {0..n} = x ^ Suc n - 1
[PROOF STEP]
by (metis atLeast0AtMost lessThan_Suc_atMost power_diff_1_eq)