DEFINITION le_false()
TYPE =
       ∀m:nat.∀n:nat.∀P:Prop.(le m n)→(le (S n) m)→P
BODY =
Show proof