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