def mod_mod

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/arith.bend:131

import Base

131# (x mod n) mod n == x mod n   (Mathlib Nat.mod_mod)
132def mod_mod(+bp: Nat, +x: Nat) -> {Nat.mod(Nat.mod(x, 1n+bp), 1n+bp) == Nat.mod(x, 1n+bp) : Nat}:
133  mod_of(0n, bp, Nat.mod(x, 1n+bp), dm_lt(bp, x))