100/arithmetic.ml

   1 (* ========================================================================= *)
   2 (* Sum of an arithmetic series.                                              *)
   3 (* ========================================================================= *)
   4
   5 let ARITHMETIC_PROGRESSION_LEMMA = prove
   6  (`!n. nsum(0..n) (\i. a + d * i) = ((n + 1) * (2 * a + n * d)) DIV 2`,
   7   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
   8
   9 let ARITHMETIC_PROGRESSION = prove
  10  (`!n. 1 <= n
  11        ==> nsum(0..n-1) (\i. a + d * i) = (n * (2 * a + (n - 1) * d)) DIV 2`,
  12   INDUCT_TAC THEN REWRITE_TAC[ARITHMETIC_PROGRESSION_LEMMA; SUC_SUB1] THEN
  13   ARITH_TAC);;