Lcm.add_succ_zero: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as Lcm
Lines 16-17 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&start_line=16&end_line=17

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

def add_succ_zero(+b: Nat, +x: Nat, +e: {Nat.add(b, 1n+x) == 0n : Nat}) -> Empty:
  N.succ_zero(Nat.add(b, x), Equal.trans(Nat, 1n+Nat.add(b, x), Nat.add(b, 1n+x), 0n, Equal.sym(Nat, Nat.add(b, 1n+x), 1n+Nat.add(b, x), A.add_succ(b, x)), e))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=succ_zero