DEFINITION blt()
TYPE =
       nat→nat→bool
BODY =
FIXblt{
         blt:nat→nat→bool
         :=λm:nat
           .λn:nat
             .<λn1:nat.bool> CASE n OF O⇒false | S n0⇒<λn1:nat.bool> CASE m OF O⇒true | S m0⇒blt m0 n0
         }