DEFINITION lt_n_O()
TYPE =
∀
n:
nat
.(
not
(
lt
n
O
))
BODY =
Show proof