let ARITHMETIC_PROGRESSION_SIMPLE = prove
 (`!n. nsum(1..n) (\i. i) = (n*(n + 1)) DIV 2`,
  INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN
  ARITH_TAC);;

horizon := 1;;

thm `;
!n. nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2
proof
  nsum(0..0) (\i. i) = 0 by NSUM_CLAUSES_NUMSEG;
    .= (0*(0 + 1)) DIV 2 [A1] by ARITH_TAC;
  now let n be num;
    assume nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2;
    nsum(0..SUC n) (\i. i) = (n*(n + 1)) DIV 2 + SUC n
      by NSUM_CLAUSES_NUMSEG,ARITH_RULE (parse_term "0 <= SUC n");
    thus .= ((SUC n)*(SUC n + 1)) DIV 2 by ARITH_TAC;
  end;
qed by INDUCT_TAC,A1`;;

thm `;
now
  (if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 [A1] by ARITH_TAC;
  nsum (1..0) (\i. i) = (0 * (0 + 1)) DIV 2 [A2]
    by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A1;
  now [A3]
    let n be num;
    assume nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A4];
    (if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2) =
      (SUC n * (SUC n + 1)) DIV 2 [A5] by ARITH_TAC;
    thus nsum (1..SUC n) (\i. i) = (SUC n * (SUC n + 1)) DIV 2 [A6]
      by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A4,A5;
  end;
  thus !n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A7] by INDUCT_TAC,A2,A3;
end`;;

let EXAMPLE = ref None;;

EXAMPLE := Some `;
!n. nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2
proof
  nsum(0..0) (\i. i) = (0*(0 + 1)) DIV 2;
  now let n be nat;
    assume nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2;
    thus nsum(0..SUC n) (\i. i) = ((SUC n)*(SUC n + 1)) DIV 2 by #;
  end;
qed`;;

thm `;
!n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2
proof
  (if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 by ARITH_TAC;
  nsum (1..0) (\i. i) = (0 * (0 + 1)) DIV 2 [A1]
    by ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG];
  !n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2
      ==> nsum (1..SUC n) (\i .i) = (SUC n * (SUC n + 1)) DIV 2
  proof
    let n be num;
    assume nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A2];
    (if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2) =
      (SUC n * (SUC n + 1)) DIV 2 by ARITH_TAC;
  qed by ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG],A2;
qed by INDUCT_TAC,A1`;;

let NSUM_CLAUSES_NUMSEG' = thm `;
!s. nsum(0..0) s = s 0 /\ !n. nsum(0..n + 1) s = nsum(0..n) s + s (n + 1)
proof
  !n. 0 <= SUC n by ARITH_TAC;
qed by NSUM_CLAUSES_NUMSEG,ADD1`;;

let num_INDUCTION' = REWRITE_RULE[ADD1] num_INDUCTION;;

thm `;
!s. (!i. s i = i) ==> !n. nsum(0..n) s = (n*(n + 1)) DIV 2
proof
  let s be num->num;
  assume !i. s i = i [A1];
  set X = \n. (nsum(0..n) s = (n*(n + 1)) DIV 2);
  nsum(0..0) s = s 0 by NSUM_CLAUSES_NUMSEG';
    .= 0 by A1;
    .= (0*(0 + 1)) DIV 2 by ARITH_TAC;
  X 0 [A2];
  now [A3] let n be num;
    assume X n;
    nsum(0..n + 1) s = (n*(n + 1)) DIV 2 + s (n + 1) by NSUM_CLAUSES_NUMSEG';
      .= (n*(n + 1)) DIV 2 + (n + 1) by A1;
    thus X (n + 1) by ARITH_TAC;
  end;
  !n. X n by MATCH_MP_TAC,num_INDUCTION',A2,A3;
qed`;;