(* ========================================================================= *)
(* Sum of an arithmetic series.                                              *)
(* ========================================================================= *)

let ARITHMETIC_PROGRESSION_LEMMA = 
prove
 (`!n. nsum(0..n) (\i. a + d * i) = ((n + 1) * (2 * a + n * d)) DIV 2`,

  INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
let ARITHMETIC_PROGRESSION = 
prove
 (`!n. 1 <= n 
       ==> nsum(0..n-1) (\i. a + d * i) = (n * (2 * a + (n - 1) * d)) DIV 2`,

  INDUCT_TAC THEN REWRITE_TAC[ARITHMETIC_PROGRESSION_LEMMA; SUC_SUB1] THEN
  ARITH_TAC);;