# 0<i => 0 < i + j proof?

If we have the natural numbers defined as:

Plus the following:

$$pred \space \_\_<\_\_ \space: Nat \times Nat$$

$$\forall i,j:Nat$$

• $$0

• $$\neg(i<0)$$

• $$suc(i) < suc(j) \Longleftrightarrow i

How to prove $$0 0 < i + j$$ by induction?

For the base case the premise fails when $$i=0$$, and thus the implication holds.

For the induction step, we assume $$i = suc(i')$$ for some $$i':Nat$$ such that $$\forall j:Nat, \space 0 0 < i' + j$$ (IH)

We assume $$0 < i$$ (H), so, we have $$0 < i => 0 < suc(i')$$

But I can't move from there, as I need to find a way to use the inductive hypothesis (IH) to complete the proof, but I don't know how. Can you help please?

• if $$j = 0$$ then $$00$$;
• otherwise, $$j = suc(j')$$ and $$0 < i \Rightarrow i+j = i+suc(j') = suc(i + j') > 0$$.