U32.internal_mod_succ_mod: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 719-721 of bend-mathlib@0.8.1.0/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/u32.bend&start_line=719&end_line=721

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

def internal_mod_succ_mod(+p: Nat, +m: Nat) -> {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+p, m) : Nat}:
  %MNat.mod_add_div(p, m) : {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+_, m) : Nat}
  Equal.sym(Nat, Nat.mod(Nat.add(1n+Nat.mod(p, m), Nat.mul(m, Nat.div(p, m))), m), Nat.mod(1n+Nat.mod(p, m), m), MNat.add_mul_mod_self_left(1n+Nat.mod(p, m), m, Nat.div(p, m)))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_mul_mod_self_left
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=mod_add_div