cancel-factor simproc allows a shorter proof

--- a/src/HOL/ex/NatSum.ML	Tue Dec 19 13:06:49 2000 +0100
+++ b/src/HOL/ex/NatSum.ML	Tue Dec 19 15:06:14 2000 +0100
@@ -93,8 +93,4 @@
 Goal "0<k ==> (k-1) * setsum (%i. k^i) (lessThan n) = k^n - 1";
 by (induct_tac "n" 1);
 by Auto_tac;
-by (subgoal_tac "1*k^n <= k * k^n" 1);
-by (Asm_full_simp_tac 1);
-by (rtac mult_le_mono1 1);
-by Auto_tac;
 qed "sum_of_powers";