Setup for the gcongr
tactic #
The core implementation of the gcongr
("generalized congruence") tactic is in the file
Tactic.GCongr.Core
. In this file we set it up for use across the library by listing
positivity
as a first-pass discharger for side goals (gcongr_discharger
).