DEFINITION le_n_O_eq()
TYPE =
       ∀n:nat.(le n O)→(eq nat O n)
BODY =
        assume n: nat
        suppose H: le n O
          by (le_O_n .)
          we proved le O n
          by (le_antisym . . previous H)
          we proved eq nat O n
       we proved ∀n:nat.(le n O)→(eq nat O n)