def pm_zero

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

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

197def pm_zero(+f: Nat, +m: Nat, +base: Nat, +acc: Nat) -> {M.pow_mod_go(f, m, 0n, base, acc) == acc : Nat}:
198  match f:
199    case 0n:
200      {==}
201    case 1n+g:
202      {==}