Word.add_inner: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as Word
Lines 133-140 of bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&start_line=133&end_line=140

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/u32alg.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

def add_inner(+n: Nat, +h: Nat, +t: Nat, +c0: Nat, +c1: Nat, +c2: Nat, +ah: Nat, +bh: Nat, +f2: {Nat.add(t, sc(n, c1)) == Nat.add(ah, bh) : Nat}, +f3: {Nat.add(h, sc(n, c2)) == Nat.add(t, c0) : Nat}) -> {Nat.add(h, Nat.add(sc(n, c1), sc(n, c2))) == Nat.add(c0, Nat.add(ah, bh)) : Nat}:
  +rhs = Nat.add(c0, Nat.add(ah, bh))
  %Equal.sym(Nat, Nat.add(h, Nat.add(sc(n, c1), sc(n, c2))), Nat.add(sc(n, c1), Nat.add(h, sc(n, c2))), NA.add_swap(h, sc(n, c1), sc(n, c2))) : {_ == rhs : Nat}
  %Equal.sym(Nat, Nat.add(h, sc(n, c2)), Nat.add(t, c0), f3) : {Nat.add(sc(n, c1), _) == rhs : Nat}
  %N.add_comm(Nat.add(t, c0), sc(n, c1)) : {_ == rhs : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(t, c0), sc(n, c1)), Nat.add(Nat.add(t, sc(n, c1)), c0), A.add_rot(t, c0, sc(n, c1))) : {_ == rhs : Nat}
  %Equal.sym(Nat, Nat.add(t, sc(n, c1)), Nat.add(ah, bh), f2) : {Nat.add(_, c0) == rhs : Nat}
  N.add_comm(Nat.add(ah, bh), c0)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend&name=add_rot
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc