Def |i| == if 0i i else -i fi

Thm* x:. |x|

Def ij == j < i

Thm* i,j:. ij

Def i < j == if i < j true ; false fi

Thm* i,j:. i < j

Def b == if b false else true fi

Thm* b:. b