Hola.
Supongo que allNat sobre n lo usás al inicio.
En la rama del existe que mencionás, tenés que eliminar el existe, reescribir en la hipótesis "sum m n = O" el valor para n luego de la eliminación del existe (que es un sucesor). Para esto usá la táctica rewrite ... in .... Luego ahí mismo podés reescribir usando SumS. Dado que ahora hay una contradicción en esta hiótesis, ya que queda un sucesor igual a cero, usás disc y seguramente symmetry para probar el goal.
Saludos, Carlos