def is_eq_add0

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:22

import Base

22def is_eq_add0(a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:
23  match a:
24    case 0n:
25      {==}
26    case 1n+k:
27      {==}