Commit 2025-06-11 23:54 d596d8c5

chore: remove last use of mono tactic (#25698) To facilitate this, add two missing gcongr lemmas: the statement of compRel_mono involves two subsets changing. For gcongr to work, there also needs to be a lemma with either just the left or just the right subset changing. In this specific instance, the gcongr proof is three lines shorter and at least as clear, hence preferrable on its own right. In general, mono is unmaintained, was only partially ported