~/jendhub

def internal_div_go_run

bend-mathlib@0.8.1.0 · nat.bend:876

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

876def internal_div_go_run(m: Nat, +a: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(a, Nat.add(m, r), 1n+d, 0n) == Nat.divmod.go(Nat.add(1n+m, a), m, d, r) : Nat & Nat}:
877  match m:
878    case 0n:
879      {==}
880    case 1n++mp:
881      %add_succ(mp, r) : {Nat.divmod.go(a, _, 1n+d, 0n) == Nat.divmod.go(1n+Nat.add(mp, a), mp, d, 1n+r) : Nat & Nat}
882      internal_div_go_run(mp, a, d, 1n+r)

Uses (5)

Used by (2)