DEFINITION le_lt_false()
TYPE =
       ∀x:nat.∀y:nat.(le x y)→(lt y x)→∀P:Prop.P
BODY =
Show proof