DEFINITION plus_permute_2_in_3()
TYPE =
       ∀x:nat.∀y:nat.∀z:nat.(eq nat (plus (plus x y) z) (plus (plus x z) y))
BODY =
        assume x: nat
        assume y: nat
        assume z: nat
          (h1) 
             (h1) 
                by (plus_assoc_r . . .)
                we proved eq nat (plus (plus x z) y) (plus x (plus z y))
                we proceed by induction on the previous result to prove eq nat (plus x (plus z y)) (plus (plus x z) y)
                   case refl_equal : ⇒
                      the thesis becomes eq nat (plus (plus x z) y) (plus (plus x z) y)
                         by (refl_equal . .)
eq nat (plus (plus x z) y) (plus (plus x z) y)
eq nat (plus x (plus z y)) (plus (plus x z) y)
             end of h1
             (h2) 
                by (plus_sym . .)
eq nat (plus y z) (plus z y)
             end of h2
             by (eq_ind_r . . . h1 . h2)
eq nat (plus x (plus y z)) (plus (plus x z) y)
          end of h1
          (h2) 
             by (plus_assoc_r . . .)
eq nat (plus (plus x y) z) (plus x (plus y z))
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat (plus (plus x y) z) (plus (plus x z) y)
       we proved ∀x:nat.∀y:nat.∀z:nat.(eq nat (plus (plus x y) z) (plus (plus x z) y))