NatOrder.az2: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder
Lines 176-178 of bend-kit-collections@0.1.4.1/nat_order.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&start_line=176&end_line=178

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

def az2(+a: Nat) -> {a == Nat.add(Nat.add(a, 0n), 0n) : Nat}:
  sy(Nat.add(Nat.add(a, 0n), 0n), a,
    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):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=sy
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=tr
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_zero