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