--- 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