law mod_mod

bend-mathlib@0.8.1.0 · nat.bend:2019

import Base

2019# Taking a remainder twice is taking it once: (a % n) % n = a % n.
2020law mod_mod:
2021  for a: Nat
2022  for n: Nat
2023  {Nat.mod(Nat.mod(a, n), n) == Nat.mod(a, n) : Nat}