~/jendhub

def internal_mod_succ_mod

bend-mathlib@0.8.1.0 · u32.bend:719

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

719def internal_mod_succ_mod(+p: Nat, +m: Nat) -> {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+p, m) : Nat}:
720  %MNat.mod_add_div(p, m) : {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+_, m) : Nat}
721  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)

Used by (1)