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 x,y \in \mathbb{N} : x \le x + y\)
le_add1: ?n ≤ ?n + ?m

Proof available

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

Proof available

Child topics