def internal_wrap_rem
bend-mathlib@0.8.1.0 · u32.bend:845
import bend-mathlib@0.8.1.0/u32.bend as U32
import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat
845def internal_wrap_rem(+b: Nat, +s: Nat, +m: Nat, +v: Nat, +hb: MNat.lt(b, m), es: {Nat.add(s, m) == v : Nat}, hv: MNat.lt(v, Nat.double(b))) -> {Nat.add(b, Nat.mod(Nat.add(s, Nat.sub(m, b)), m)) == v : Nat}:
846 +y = Nat.add(s, Nat.sub(m, b))
847 +ey = internal_wrap_sum(b, s, m, v, hb, es)
848 +hy = internal_rem_lt(b, y, v, ey, hv)
849 %Equal.sym(Nat, Nat.mod(y, m), y, MNat.mod_eq_of_lt(y, m, MNat.lt_trans(y, b, m, hy, hb))) : {Nat.add(b, _) == v : Nat}
850 ey