[STATEMENT]
lemma "1 * (2 * x + (y::nat) + 0 + 1) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * (2 * x + y + 0 + 1) \<noteq> 0
[PROOF STEP]
apply (reify Inum_eqs ("1 * (2 * x + (y::nat) + 0 + 1)"))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inum (Mul 1 (Add (Add (Add (Mul 2 (Var (Suc (Suc (Suc 0))))) (Var (Suc (Suc 0)))) (Var (Suc 0))) (Var 0))) [1, 0, y, x] \<noteq> 0
[PROOF STEP]
oops