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

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

def F_mono(p: Lin, q: Lin, v: Vs, +h: {lle(p, q) == True{} : Bool}) -> LE(F(p, v), F(q, v)):
  match p q v:
    case L{+a0, +a1, +a2, +a3, +a4} L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
      +l0 = Nat.is_le(a0, b0)
      +l1 = Nat.is_le(a1, b1)
      +l2 = Nat.is_le(a2, b2)
      +l3 = Nat.is_le(a3, b3)
      +l4 = Nat.is_le(a4, b4)
      +r1 = and5_r(l0, l1, l2, l3, l4, h)
      +r2 = MBool.eq_true_of_and_right(l1, Bool.and(l2, Bool.and(l3, l4)), r1)
      +r3 = MBool.eq_true_of_and_right(l2, Bool.and(l3, l4), r2)
      +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)
      MNat.add_le_add(a0, Nat.add(x1, Nat.add(x2, Nat.add(x3, x4))), b0, Nat.add(y1, Nat.add(y2, Nat.add(y3, y4))), and5_1(l0, l1, l2, l3, l4, h), MNat.add_le_add(x1, Nat.add(x2, Nat.add(x3, x4)), y1, Nat.add(y2, Nat.add(y3, y4)), MNat.mul_le_mul_right(a1, b1, v1, MBool.eq_true_of_and_left(l1, Bool.and(l2, Bool.and(l3, l4)), r1)), MNat.add_le_add(x2, Nat.add(x3, x4), y2, Nat.add(y3, y4), MNat.mul_le_mul_right(a2, b2, v2, MBool.eq_true_of_and_left(l2, Bool.and(l3, l4), r2)), MNat.add_le_add(x3, x4, y3, y4, MNat.mul_le_mul_right(a3, b3, v3, MBool.eq_true_of_and_left(l3, l4, r3)), MNat.mul_le_mul_right(a4, b4, v4, MBool.eq_true_of_and_right(l3, l4, r3))))))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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.is_le
  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=LE
  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=and5_1
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=and5_r
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=lle
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_true_of_and_left
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=eq_true_of_and_right
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_le_add
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=mul_le_mul_right