DEFINITION O_S()
TYPE =
       ∀n:nat.(not (eq nat O (S n)))
BODY =
       assume n: nat
          we must prove not (eq nat O (S n))
          or equivalently (eq nat O (S n))→False
          suppose H: eq nat O (S n)
             by (sym_eq . . . H)
             we proved eq nat (S n) O
             we proceed by induction on the previous result to prove IsSucc O
                case refl_equal : ⇒
                   the thesis becomes IsSucc (S n)
                      consider I
                      we proved True
IsSucc (S n)
             we proved IsSucc O
             that is equivalent to False
          we proved (eq nat O (S n))→False
          that is equivalent to not (eq nat O (S n))
       we proved ∀n:nat.(not (eq nat O (S n)))