NatOrder.F_add: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder
Lines 83-103 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=83&end_line=103

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

def F_add(p: Lin, q: Lin, v: Vs) -> {Nat.add(F(p, v), F(q, v)) == F(ladd(p, q), v) : Nat}:
  match p q v:
    case L{+a0, +a1, +a2, +a3, +a4} L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
      +x1 = Nat.mul(a1, v1)
      +x2 = Nat.mul(a2, v2)
      +x3 = Nat.mul(a3, v3)
      +x4 = Nat.mul(a4, v4)
      +y1 = Nat.mul(b1, v1)
      +y2 = Nat.mul(b2, v2)
      +y3 = Nat.mul(b3, v3)
      +y4 = Nat.mul(b4, v4)
      +z1 = Nat.mul(Nat.add(a1, b1), v1)
      +z2 = Nat.mul(Nat.add(a2, b2), v2)
      +z3 = Nat.mul(Nat.add(a3, b3), v3)
      +z4 = Nat.mul(Nat.add(a4, b4), v4)
      step(a0, Nat.add(x1, Nat.add(x2, Nat.add(x3, x4))), b0, Nat.add(y1, Nat.add(y2, Nat.add(y3, y4))),
        Nat.add(a0, b0), Nat.add(z1, Nat.add(z2, Nat.add(z3, z4))), {==},
        step(x1, Nat.add(x2, Nat.add(x3, x4)), y1, Nat.add(y2, Nat.add(y3, y4)), z1,
          Nat.add(z2, Nat.add(z3, z4)), MNat.add_mul_sym(a1, b1, v1),
          step(x2, Nat.add(x3, x4), y2, Nat.add(y3, y4), z2, Nat.add(z3, z4), MNat.add_mul_sym(a2, b2, v2),
            step(x3, x4, y3, y4, z3, z4, MNat.add_mul_sym(a3, b3, v3), MNat.add_mul_sym(a4, b4, v4)))))

Uses (9):
  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=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=F
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=Lin
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=Vs
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=ladd
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_mul_sym