[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)
into:
a + suc b == b + suc a
which would end my proof. How can I do that?
Janek
More information about the Agda
mailing list