DEFINITION minus_Sx_SO()
TYPE =
       ∀x:nat.(eq nat (minus (S x) (S O)) x)
BODY =
       assume x: nat
          by (minus_n_O .)
          we proved eq nat x (minus x O)
          we proceed by induction on the previous result to prove eq nat (minus x O) x
             case refl_equal : ⇒
                the thesis becomes eq nat x x
                   by (refl_equal . .)
eq nat x x
          we proved eq nat (minus x O) x
          that is equivalent to eq nat (minus (S x) (S O)) x
       we proved ∀x:nat.(eq nat (minus (S x) (S O)) x)