[Agda] Proving a + suc b == b + suc a

[Jan Stolarek]

Hi *,

I'm trying to prove that: a + suc b == b + suc a. I see the solution on paper, but I don't know 
how to express it in Agda:

1. From the commutativity of addition (+comm a b) I know that:
    a + b == b + a
2. Using congruence I know that
    suc (a + b) == suc (b + a)
3. I also know +suc, which proves that:
    suc (a + b) = a + suc b

Now if I could apply +suc to both sides of (cong suc (+comm a b)) I would turn:
    suc (a + b) == suc (b + a)
into:
    a + suc b == b + suc a
which would end my proof. How can I do that?

Janek