def inv_go
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as Naturalimport Base
305def inv_go(fuel: Nat, +m: Nat, +r0: Nat, +s0: Nat, +r1: Nat, +s1: Nat) -> Bezout:
306 match fuel r1:
307 case 0n _:
308 BZ{r0, s0}
309 case 1n+f 0n:
310 BZ{r0, s0}
311 case 1n+f 1n+ +rp:
312 inv_go(f, m, 1n+rp, s1, Nat.mod(r0, 1n+rp), inv_step(m, Nat.div(r0, 1n+rp), s0, s1))
Uses (5)
Used by (7)
- bend-collections-laws-crypto@1.0.0.0/src/math/natural:mod_inverse
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse:inv_bz
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse:inv_r
- bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse:inv_inv
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel:inv_fuel
- …