This implements the greedy translation-invariant construction for 1518. I also introduced a file FreshGenerator.lean that contains convenient lemmas about the "fresh generators" in a free group of infinite rank. At the moment, I can detect simple inequalities in the free group, more or less the ones that one obtains by taking the map to Z that sends the fresh generator to 1 and all other generators to 0.
This implements the greedy translation-invariant construction for 1518. I also introduced a file
FreshGenerator.leanthat contains convenient lemmas about the "fresh generators" in a free group of infinite rank. At the moment, I can detect simple inequalities in the free group, more or less the ones that one obtains by taking the map toZthat sends the fresh generator to 1 and all other generators to 0.Closes #661