DEFINITION le_bge()
TYPE =
∀
x:
nat
.
∀
y:
nat
.(
le
x y)
→
(
eq
bool
(
blt
y x)
false
)
BODY =
Show proof