let EXAMPLE = prove (`!n. nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2`, INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);; let EXAMPLE_IN_MIZAR_LIGHT = thm `; !n. nsum (0..n) (\i. i) = (n * (n + 1)) DIV 2 [1] proof nsum (0..0) (\i. i) = 0 [2] by NSUM_CLAUSES_NUMSEG; ... = (0 * (0 + 1)) DIV 2 [3] by ARITH_TAC; !n. nsum (0..n) (\i. i) = (n * (n + 1)) DIV 2 ==> nsum (0..SUC n) (\i. i) = (SUC n * (SUC n + 1)) DIV 2 [4] proof let n be num; assume nsum (0..n) (\i. i) = (n * (n + 1)) DIV 2 [5]; qed by #; qed by INDUCT_TAC from 3,4`;;