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

Jan Stolarek jan.stolarek at p.lodz.pl
Wed Nov 13 12:27:36 CET 2013

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)
    a + suc b == b + suc a
which would end my proof. How can I do that?


More information about the Agda mailing list