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

Andrea Vezzosi sanzhiyan at gmail.com
Wed Nov 13 18:55:38 CET 2013

On Wed, Nov 13, 2013 at 12:27 PM, Jan Stolarek <jan.stolarek at p.lodz.pl>wrote:

> [...]
> 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?
>
>
To chain proofs like that you can use transitivity:

trans : forall {A}{x y z : A} -> x == y -> y == z -> x == z
trans refl eq = eq

in fact you'll need to nest them to apply something on both sides:

trans (....) (trans (cong suc (+comm a b)) (....))

(Usually at this point the thing gets less than readable and we use the
prettier syntax provided by ≡-Reasoning in
Relation.Binary.PropositionalEquality from the stdlib.)

-- Andrea

> Janek
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131113/7ae76819/attachment.html