1 (* ========================================================================= *)
2 (* Sum of an arithmetic series. *)
3 (* ========================================================================= *)
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);;
9 let ARITHMETIC_PROGRESSION = prove
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