def one_mul

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/semiring.bend:15

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

15def one_mul(+x: Nat) -> {Nat.mul(1n, x) == x : Nat}:
16  NA.add_zero(x)