If we have the natural numbers defined as:
Plus the following:
$pred \space \_\_<\_\_ \space: Nat \times Nat$
$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?