def inv_inv

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

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

97def inv_inv(fuel: Nat, +mp: Nat, +a: Nat, +r0: Nat, +s0: Nat, +r1: Nat, +s1: Nat, +h0: {Nat.mod(Nat.mul(a, s0), 1n+mp) == Nat.mod(r0, 1n+mp) : Nat}, +h1: {Nat.mod(Nat.mul(a, s1), 1n+mp) == Nat.mod(r1, 1n+mp) : Nat}) -> {Nat.mod(Nat.mul(a, bc(M.inv_go(fuel, 1n+mp, r0, s0, r1, s1))), 1n+mp) == Nat.mod(bg(M.inv_go(fuel, 1n+mp, r0, s0, r1, s1)), 1n+mp) : Nat}:
98  match fuel r1:
99    case 0n 0n:
100      h0
101    case 0n 1n+rp:
102      h0
103    case 1n+f 0n:
104      h0
105    case 1n+ +f 1n+ +rp:
106      inv_inv(f, mp, a, 1n+rp, s1, Nat.mod(r0, 1n+rp), M.inv_step(1n+mp, Nat.div(r0, 1n+rp), s0, s1), h1, inv_step_ok(mp, a, r0, s0, rp, s1, h0, h1))