def zero_add

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:44

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

44def zero_add(+x: Nat) -> {Nat.add(0n, x) == x : Nat}:
45  Equal.trans(Nat, Nat.add(0n, x), Nat.add(x, 0n), x, N.add_comm(0n, x), N.add_zero(x))