def zmul
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as Precimport Base
137def zmul(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}:
138 {==}
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as Precimport Base
137def zmul(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}:
138 {==}