If we have the natural numbers defined as:

enter image description here

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?


1 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$.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.