def one_mul

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/arith.bend:78

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

78def one_mul(+d: Nat) -> {Nat.mul(1n, d) == d : Nat}:
79  N.add_zero(d)