NUM_SIMPLIFY_CONV : conv
# NUM_SIMPLIFY_CONV `~(n = 0) ==> PRE(n) + 1 = n`;; val it : thm = |- ~(n = 0) ==> PRE n + 1 = n <=> (!m. ~(n = SUC m) /\ (~(m = 0) \/ ~(n = 0)) \/ n = 0 \/ m + 1 = n)
# ARITH_RULE `~(n = 0) ==> n DIV 3 < n`;; val it : thm = |- ~(n = 0) ==> n DIV 3 < n