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

Thm* i,j:. i < j