An evidence of $n \le m$. refl+step definition.

Convert from zero+succ to refl+step definition.

Inverse of toZeroSucc.

Convert refl+step to zero+succ definition.

Inverse of fromZeroSucc.

Find the LEProof n m, i.e. compare numbers.

$\forall n : \mathbb{N}, 0 \le n$

$\forall n\, m : \mathbb{N}, n \le m \to 1 + n \le 1 + m$

$\forall n : \mathbb{N}, n \le n$

$\forall n\, m : \mathbb{N}, n \le m \to n \le 1 + m$

$\forall n\, m : \mathbb{N}, n \le m \to m \le n \to n \equiv m$

$\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p$

$\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n$

$\forall n\, m : \mathbb{N}, n \le m \to \neg (1 + m \le n)$

$\forall n\, m : \mathbb{N}, 1 + n \le m \to n \le m$

$\forall n\, m : \mathbb{N}, 1 + n \le 1 + m \to n \le m$

$\forall n\ : \mathbb{N}, n \le 0 \to n \equiv 0$