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

[Nils Anders Danielsson]

On 2013-11-13 18:55, Andrea Vezzosi wrote:
> 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.)

See, for instance, README.Nat:

   http://www.cse.chalmers.se/~nad/listings/lib/README.Nat.html

-- 
/NAD