def iz_add

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/canon.bend:127

import Base

127def iz_add(+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}:
128  match a:
129    case 0n:
130      {==}
131    case 1n+q:
132      {==}