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