# let LEMMA_1 = prove
 (`!x n. x pow (n + 1) - (&n + &1) * x + &n =
         (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`,
  CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN INDUCT_TAC THEN
  REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL
   [REAL_ARITH_TAC; REWRITE_TAC[ARITH_RULE `1 <= SUC n`]] THEN
  SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN
  REWRITE_TAC[real_pow; REAL_MUL_RID] THEN
  REWRITE_TAC[REAL_ARITH `k * x * x pow n = (k * x pow n) * x`] THEN
  ASM_REWRITE_TAC[SUM_RMUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC);;
val ( LEMMA_1 ) : thm =
  |- !x n.
         x pow (n + 1) - (&n + &1) * x + &n =
         (x - &1) pow 2 * sum (1..n) (\k. &k * x pow (n - k))

# print_executed_proof ();;
e ((CONV_TAC (ONCE_DEPTH_CONV SYM_CONV)) THEN GEN_TAC THEN INDUCT_TAC THEN (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]) THENL [REAL_ARITH_TAC; REWRITE_TAC [ARITH_RULE `1 <= SUC n`]] THEN (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]) THEN (REWRITE_TAC [real_pow;REAL_MUL_RID]) THEN (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]) THEN (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]) THEN (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]) THEN REAL_ARITH_TAC);;

val it : unit = () 
# print_flat_proof ();;
e (CONV_TAC (ONCE_DEPTH_CONV SYM_CONV));;
e (GEN_TAC);;
e (INDUCT_TAC);;
e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
e (REAL_ARITH_TAC);;
e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);;
e (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]);;
e (REWRITE_TAC [real_pow;REAL_MUL_RID]);;
e (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]);;
e (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]);;
e (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]);;
e (REAL_ARITH_TAC);;