DEFINITION minus_n_O()
TYPE =
       ∀n:nat.(eq nat n (minus n O))
BODY =
       assume n: nat
          we proceed by induction on n to prove eq nat n (minus n O)
             case O : ⇒
                the thesis becomes eq nat O (minus O O)
                   by (refl_equal . .)
                   we proved eq nat O O
eq nat O (minus O O)
             case S : n0:nat ⇒
                the thesis becomes eq nat (S n0) (minus (S n0) O)
                () by induction hypothesis we know eq nat n0 (minus n0 O)
                   by (refl_equal . .)
                   we proved eq nat (S n0) (S n0)
eq nat (S n0) (minus (S n0) O)
          we proved eq nat n (minus n O)
       we proved ∀n:nat.(eq nat n (minus n O))