Order.internal_nat_le_trans4: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/order.bend as Order
Lines 102-103 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=102&end_line=103

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

def internal_nat_le_trans4(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e: Nat, ab: MNat.le(a, b), bc: MNat.le(b, c), cd: MNat.le(c, d), de: MNat.le(d, e)) -> MNat.le(a, e):
  le_trans4(~Nat, ~Nat.is_le, ~MNat.le_trans, a, b, c, d, e, ab, bc, cd, de)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/order.bend&name=le_trans4