def inv_r

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/inverse.bend:108

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

108# the remainders are Euclid's
109def inv_r(fuel: Nat, +m: Nat, +r0: Nat, +s0: Nat, +r1: Nat, +s1: Nat) -> {bg(M.inv_go(fuel, m, r0, s0, r1, s1)) == M.gcd_go(fuel, r0, r1) : Nat}:
110  match fuel r1:
111    case 0n 0n:
112      {==}
113    case 0n 1n+rp:
114      {==}
115    case 1n+f 0n:
116      {==}
117    case 1n+ +f 1n+ +rp:
118      inv_r(f, m, 1n+rp, s1, Nat.mod(r0, 1n+rp), M.inv_step(m, Nat.div(r0, 1n+rp), s0, s1))