The tactic symmetry

symmetry

The conclusion of the current proof must be an equality.

It swaps the two sides of the equalityusing the symmetric property.

None.