Order.le_trans4: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/order.bend as Order
Lines 22-36 of bend-mathlib@0.8.1.0/order.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/order.bend&start_line=22&end_line=36

import Base

# A chain of four comparisons composes.
law le_trans4:
  for ~A: Data
  for ~le: A -> A -> Bool
  for ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}
  for +a: A
  for +b: A
  for +c: A
  for +d: A
  for +e: A
  for ab: {le(a, b) == True{} : Bool}
  for bc: {le(b, c) == True{} : Bool}
  for cd: {le(c, d) == True{} : Bool}
  for de: {le(d, e) == True{} : Bool}
  {le(a, e) == True{} : Bool}

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/order.bend&name=le_trans3