Jakub Kądziołka (Feb 07 2021 at 11:58): Jakub Kądziołka (Feb 07 2021 at 11:58):is there a tactic or simproc that will use [a = b] (mod n) to rewrite, say, [a^k * (a + c) = a^a] (mod n) into [b^k * (b + c) = b^a] (mod n)? I'm getting just about annoyed enough to try writing one myself, but I'd rather avoid it if it already exists somewhere.
Manuel Eberl (Feb 07 2021 at 13:29):Rewriting w.r.t. relations other than equality is one of those things that would be nice to have. I think we had a couple of students working on this sort of thing but somehow we never got something finished out of it (I think?).
Personally, I usually just do chains of [_ = _] (mod _) using also just like I would do with regular equations and show each step using cong_add, cong_diff, etc.
Last updated: Dec 21 2024 at 16:20 UTC