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 that you have read and understand our privacy policy and code of conduct.

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