INDUCT_TAC : tactic
A ?- !n. P ======================================== INDUCT_TAC A ?- P[0/n] A u {P} ?- P[SUC n'/n]
# g `!n. nsum(1..n) (\i. i) = (n * (n + 1)) DIV 2`;;
# e INDUCT_TAC;; val it : goalstack = 2 subgoals (2 total) 0 [`nsum (1 .. n) (\i. i) = (n * (n + 1)) DIV 2`] `nsum (1 .. SUC n) (\i. i) = (SUC n * (SUC n + 1)) DIV 2` `nsum (1 .. 0) (\i. i) = (0 * (0 + 1)) DIV 2`
# e(ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;