DEFINITION lt_x_O()
TYPE =
∀
x:
nat
.(
lt
x
O
)
→
∀
P:
Prop
.P
BODY =
Show proof