DEFINITION minus_n_n()
TYPE =
       ∀n:nat.(eq nat O (minus n n))
BODY =
       assume n: nat
          we proceed by induction on n to prove eq nat O (minus n n)
             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 O (minus (S n0) (S n0))
                (IHn) by induction hypothesis we know eq nat O (minus n0 n0)
                   consider IHn
                   we proved eq nat O (minus n0 n0)
eq nat O (minus (S n0) (S n0))
          we proved eq nat O (minus n n)
       we proved ∀n:nat.(eq nat O (minus n n))