Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. A much shorter proof exists if the "divides" relation || can be used, see addmodlteqALT . (Contributed by AV, 20-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | addmodlteq | |