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

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

def internal_nat_le_trans3(+a: Nat, +b: Nat, +c: Nat, +d: Nat, ab: MNat.le(a, b), bc: MNat.le(b, c), cd: MNat.le(c, d)) -> MNat.le(a, d):
  le_trans3(~Nat, ~Nat.is_le, ~MNat.le_trans, a, b, c, d, ab, bc, cd)

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_trans3