Flipping hypothesis around equals sign

Stream: new members

[Andrew Helwer]

Quick question, if I have a hypothesis h : a = a + b how can I rewrite it to be h : a + b = a?

[Jon Eugster]

eq.symm is the relevant piece, so for example h.symm

[Ruben Van de Velde]

Or if you do want to rewrite, rw eq_comm. It's a general pattern that X.symm is an implication and X_comm is the iff