DEFINITION minus_x_SO()
TYPE =
       ∀x:nat.(lt O x)→(eq nat x (S (minus x (S O))))
BODY =
        assume x: nat
        suppose H: lt O x
          by (minus_x_Sy . . H)
          we proved eq nat (minus x O) (S (minus x (S O)))
          we proceed by induction on the previous result to prove eq nat x (S (minus x (S O)))
             case refl_equal : ⇒
                the thesis becomes eq nat x (minus x O)
                   by (minus_n_O .)
                   we proved eq nat x (minus x O)
                   we proceed by induction on the previous result to prove eq nat x (minus x O)
                      case refl_equal : ⇒
                         the thesis becomes eq nat x x
                            by (refl_equal . .)
eq nat x x
eq nat x (minus x O)
          we proved eq nat x (S (minus x (S O)))
       we proved ∀x:nat.(lt O x)→(eq nat x (S (minus x (S O))))