DEFINITION blt_lt()
TYPE =
       ∀x:nat.∀y:nat.(eq bool (blt y x) true)→(lt y x)
BODY =
Show proof