~/jendhub

def internal_div_go_shift

bend-mathlib@0.8.1.0 · nat.bend:867

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

867def internal_div_go_shift(n: Nat, m: Nat, +d: Nat, +r: Nat) -> {1n+Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)) == Pair.fst(Nat, Nat, Nat.divmod.go(n, m, 1n+d, r)) : Nat}:
868  match n m:
869    case 0n _:
870      {==}
871    case 1n+np 0n:
872      internal_div_go_shift(np, r, 1n+d, 0n)
873    case 1n+np 1n+mp:
874      internal_div_go_shift(np, mp, d, 1n+r)

Uses (3)

Used by (1)