DEFINITION le_n_O_eq()
TYPE =
∀
n:
nat
.(
le
n
O
)
→
(
eq
nat
O
n)
BODY =
Show proof