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

Question

If we have the natural numbers defined as:

Plus the following:

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

$\forall i,j:Nat$

• $0<suc(j)$

• $\neg(i<0)$

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

How to prove $0<i => 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<i' => 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?

Answer 1

There is no need for an induction here.

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