def gz

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

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

49# two fuels that both reach the end give the same gcd
50def gz(+f: Nat, +a: Nat) -> {M.gcd_go(f, a, 0n) == a : Nat}:
51  match f:
52    case 0n:
53      {==}
54    case 1n+g:
55      {==}