symmetry

symmetry is used to swap the left and right sides of an equality.

symmetry can be used on either the goal or a list of hypotheses.

Syntax

(* Usage on goal *)
symmetry.

(* Usage on hypotheses *)
symmetry in H.
symmetry in H1, H2.

Examples

Before

=========================
1/1
5 = 2 + 3

symmetry.

After

=========================
1/1
2 + 3 = 5

Resources

Reference Documentation

---