Functional proofs (Haskell)

I failed at reading RWH; and not one to quit, I ordered Haskell: The Craft of Functional Programming. Now I'm curious about these functional proofs on page 146. Specifically I'm trying to prove 8.5.1 sum (reverse xs) = sum xs. I can do some of the induction proof but then I get stuck..

HYP:

sum ( reverse xs ) = sum xs

BASE:

sum ( reverse [] ) = sum []

Left  = sum ( [] ) (reverse.1)
      = 0          (sum.1)

Right = 0          (sum.1)

INDUCTION:

sum ( reverse (x:xs) ) = sum (x:xs) 

Left = sum ( reverse xs ++ [x] )    (reverse.2)

Right = sum (x:xs)   
      = x + sum xs                  (sum.2)

So now I'm just trying ot prove that Left sum ( reverse xs ++ [x] ) is equal to Right x + sum xs, but that isn't too far off from where I started sum ( reverse (x:xs) ) = sum (x:xs).

I'm not quite sure why this needs to be proved, it seems totally reasonable to use the symbolic proof of reverse x:y:z = z:y:x (by defn), and because + is commutative (arth) then reverse 1+2+3 = 3+2+1,