[STATEMENT]
lemma "x - (0::int) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - 0 = x
[PROOF STEP]
nitpick [unary_ints, expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - 0 = x
[PROOF STEP]
nitpick [binary_ints, expect = none]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x - 0 = x
[PROOF STEP]
sorry