~/jendhub

def mul1

bend-collections-laws-math@1.0.0.0 · proofs/math/number/prime.bend:102

import bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend as Prime
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A

102def mul1(+x: Nat) -> {Nat.mul(1n, x) == x : Nat}:
103  Equal.trans(Nat, Nat.mul(1n, x), Nat.mul(x, 1n), x, A.mul_comm(1n, x), A.mul_one(x))

Uses (5)

Used by (1)