def mul1

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natlight.bend:31

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

31def mul1(+y: Nat) -> {Nat.mul(1n, y) == y : Nat}:
32  Equal.trans(Nat, Nat.mul(1n, y), Nat.mul(y, 1n), y, NA.mul_comm(1n, y), NA.mul_one(y))