def mod_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:72

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

72def mod_shift(+N0: Nat, +bp: Nat, +t: Nat) -> {Nat.mod(C.shift(t, Nat.mod(N0, 1n+bp)), 1n+bp) == Nat.mod(C.shift(t, N0), 1n+bp) : Nat}:
73  +B = Nat.add(1n, bp)
74  +e1 = Equal.cong(Nat, Nat, u => Nat.mod(u, B), C.shift(t, N0), Nat.add(Nat.mul(C.shift(t, Nat.div(N0, B)), B), C.shift(t, Nat.mod(N0, B))), shq(N0, bp, t))
75  Equal.sym(Nat, Nat.mod(C.shift(t, N0), B), Nat.mod(C.shift(t, Nat.mod(N0, B)), B), Equal.trans(Nat, Nat.mod(C.shift(t, N0), B), Nat.mod(Nat.add(Nat.mul(C.shift(t, Nat.div(N0, B)), B), C.shift(t, Nat.mod(N0, B))), B), Nat.mod(C.shift(t, Nat.mod(N0, B)), B), e1, mod_mul_add(C.shift(t, Nat.div(N0, B)), bp, C.shift(t, Nat.mod(N0, B)))))