def iv_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:220

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

220def iv_zero(+f: Nat, +m: Nat, +r0: Nat, +s0: Nat, +s1: Nat) -> {M.inv_go(f, m, r0, s0, 0n, s1) == M.BZ{r0, s0} : M.Bezout}:
221  match f:
222    case 0n:
223      {==}
224    case 1n+g:
225      {==}