DEFINITION le_O_n()
TYPE =
       ∀n:nat.(le O n)
BODY =
       assume n: nat
          we proceed by induction on n to prove le O n
             case O : ⇒
                the thesis becomes le O O
                   by (le_n .)
le O O
             case S : n0:nat ⇒
                the thesis becomes le O (S n0)
                (IHn) by induction hypothesis we know le O n0
                   by (le_S . . IHn)
le O (S n0)
          we proved le O n
       we proved ∀n:nat.(le O n)