~/jendhub

def sp.snd_go

bend-osdev-cbc@0.1.0.0 · PROOF.bend:110

import bend-osdev-cbc@0.1.0.0/PROOF.bend as PROOF
import Base

110def sp.snd_go(n: Nat, m: Nat, d1: Nat, d2: Nat, r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d1, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d2, r)) : Nat}:
111  match n:
112    case 0n:
113      {==}
114    case 1n+np:
115      match m:
116        case 0n:
117          sp.snd_go(np, r, 1n+d1, 1n+d2, 0n)
118        case 1n+mp:
119          sp.snd_go(np, mp, d1, d2, 1n+r)

Uses (3)

Used by (1)