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.
Matita Home