~/jendhub

def zero_add

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix64.bend:45

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

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

Uses (5)

Used by (1)