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

[Martin Escardo]

On 13/11/13 11:27, Jan Stolarek wrote:
> 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?

You don't need to do anything in the last step, because both equations 
are definitionally the same. You are done.

M.