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