def m1

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/rconst.bend:91

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

91def m1(+x: Nat) -> {Nat.mul(1n, x) == x : Nat}:
92  SR.one_mul(x)