Setup for the gcongr tactic

The core implementation of the gcongr ("generalized congruence") tactic is in the file Tactic.GCongr.Core.

We also use assumption to discharge side goals. In a further downstream file, positivity will also be registered as a discharger. From that point, positivity will be tried before assumption is: that is perfectly fine.

We register gcongr with the hint tactic.