~/jendhub

def internal_mod_go_d

bend-mathlib@0.8.1.0 · nat.bend:2034

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

2034def internal_mod_go_d(n: Nat, m: Nat, -d: Nat, -e: Nat, r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(n, m, e, r)) : Nat}:
2035  match n m:
2036    case 0n _:
2037      {==}
2038    case 1n+np 0n:
2039      internal_mod_go_d(np, r, 1n+d, 1n+e, 0n)
2040    case 1n+np 1n+mp:
2041      internal_mod_go_d(np, mp, d, e, 1n+r)

Uses (3)

Used by (1)