agda
Create a version of [m+kn]%n≡m%n for integers
Working on modular arithmetic, to prove that the setoid of integers modulo m (for nonzero m), I find myself looking for something like [a+kn]%n≡a%n : ∀ a k n .{{_ : NonZero n}} → (a + k * n) % n ≡ a % n in Data.Integer.DivMod. I've found this difficult to prove myself.
Having looked at something similar, it seems to be a horrid case analysis on k. I wonder if it might be easier to redefine _%ℕ_ and _/ℕ_ on integers to delegate to the naturals via the signed representation instead of the current versions? (Which seem to recapitulate/inline the signAbs view construction?) #2878
I'm pretty sure Conor and I have code for this somewhere. A direct proof is horrible. There's a proof via symmetric difference and a worker helper that does a rather complex recursion that is not horrid. [Coming up with that worker, that's pure Conor genius.] There are things quite close here. Hmm, it might be we had something even closer in a previous version (we're obsessive refactorers).
