def bl_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:372

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

372def bl_zero(f: Nat, +a: Nat) -> {nbloop(f, a, 0n, True{}, nsm(a, 0n)) == M.gcd(a, 0n) : Nat}:
373  match f:
374    case 0n:
375      {==}
376    case 1n+g:
377      {==}