# HG changeset patch
# User huffman
# Date 1176688935 -7200
# Node ID 3ea6c1cb3dab16e70cb463c7937516c2159ec75d
# Parent  8f2ba236918b8883ae9326e03ba20a453082767a
generalized type of lemma geometric_sum

diff -r 8f2ba236918b -r 3ea6c1cb3dab src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sun Apr 15 23:25:55 2007 +0200
+++ b/src/HOL/SetInterval.thy	Mon Apr 16 04:02:15 2007 +0200
@@ -738,10 +738,11 @@
 
 lemma geometric_sum:
   "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
-  (x ^ n - 1) / (x - 1::'a::{field, recpower, division_by_zero})"
+  (x ^ n - 1) / (x - 1::'a::{field, recpower})"
   apply (induct "n", auto)
   apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
   apply (auto simp add: mult_assoc left_distrib)
+  apply (simp add: times_divide_eq_right [symmetric] divide_self)
   apply (simp add: right_distrib diff_minus mult_commute power_Suc)
   done