# Exercise D2, Cook and Nguyen, Logical Foundations of Proof Complexity

Cook and Nguyen, Logical Foundations of Proof Complexity, on p. 42, ask for a proof in $$I \Delta_0$$ of $$\exists z(x + z = y \lor y + z = x)$$, and give as hint, "Induction on $$x$$. Base case: B2, O2. Induction step: B3, B4, D1."

The obvious induction predicate is $$\phi(x)$$ as $$\exists z(x + z = y \lor y + z = x)$$, only the quantifier isn't bounded. So it seems one needs to prove: $$\exists z≤y(x + z = y) \lor \exists z≤ x(y + z = x)$$. But, trying to prove this, I would like to use transitivity of $$≤$$ at some point. But transitivity is proved later, as D4, and the hints of the proof of D4 rely on D3, which rely on D2.

Am I missing something simple, or worse am I misunderstanding something simple?

D3 is $$x ≤ y \iff \exists z(x + z =y)$$