def internal_nat_le_trans4

bend-mathlib@0.8.1.0 · order.bend:102

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

102def 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):
103  le_trans4(~Nat, ~Nat.is_le, ~MNat.le_trans, a, b, c, d, e, ab, bc, cd, de)