def az2

bend-kit-collections@0.1.4.1 · nat_order.bend:176

import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

176def az2(+a: Nat) -> {a == Nat.add(Nat.add(a, 0n), 0n) : Nat}:
177  sy(Nat.add(Nat.add(a, 0n), 0n), a,
178    tr(Nat.add(Nat.add(a, 0n), 0n), Nat.add(a, 0n), a, MNat.add_zero(Nat.add(a, 0n)), MNat.add_zero(a)))

Uses (5)

Used by (3)