Commit 2024-01-08 12:05 006e9a36

View on Github →

chore: Move a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m (#9505) Those lemmas were very recently added in #9397. Also make them iffs and golf. Part of #9411

Estimated changes