PR !4#25765: feat(gcongr): lemma for rewriting inside div...

Stream: triage

[Random Issue Bot]

Today I chose PR #25765 for discussion!

feat(gcongr): lemma for rewriting inside divisibility
Created by @Jovan Gerbscheid (@JovanGerb) on 2025-06-12
Labels: delegated, t-data

Is this PR still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

Just waiting for @Jovan Gerbscheid to add a test :wink:

[Jovan Gerbscheid]

The issue is that there are 2 very distinct ways to grw in the RHS of a divisibility relation. You can rewrite with congruence mod n, as the PR shows, but you can also rewrite with another divisibility relation. In the current implementation, these two options cannot co-exist.

What I would like, is that grw can check if the used relation is symmetric, and if so, prove an iff instead of just an implication. That way, these two grw options will both be available.

So tldr, it depends on some other PR that I haven't made yet.