def internal_nat_le_trans3

bend-mathlib@0.8.1.0 · order.bend:99

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

99def 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):
100  le_trans3(~Nat, ~Nat.is_le, ~MNat.le_trans, a, b, c, d, ab, bc, cd)