Order theory


THEOREM    \(\forall n \in \mathbb{N} : 0 \le n\)
le0: 0 ≤ ?n

Proof unavailable

THEOREM    \(\forall m,n \in \mathbb{N} : m \lt n \Rightarrow \Suc(m) \lt \Suc(n)\)
Suc_mono: ?m < ?n \(\Longrightarrow\) Suc ?m < Suc ?n

Proof unavailable

THEOREM    \(\forall m,n \in \mathbb{N} : n \le n + m\)
le_add1: ?n ≤ ?n + ?m

Proof unavailable

THEOREM    \(\forall m,n \in \mathbb{N} : n \le m + n\)
le_add2: ?n ≤ ?m + ?n

Proof unavailable