~/jendhub

def mul0

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

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

99def mul0(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}:
100  Equal.trans(Nat, Nat.mul(0n, x), Nat.mul(x, 0n), 0n, A.mul_comm(0n, x), A.mul_zero(x))

Uses (5)

Used by (1)