def internal_le_trans_nat

bend-mathlib@0.8.1.0 · sort.bend:52

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

52def internal_le_trans_nat(x: Nat, y: Nat, z: Nat, xy: {Nat.is_le(x, y) == True{} : Bool}, yz: {Nat.is_le(y, z) == True{} : Bool}) -> {Nat.is_le(x, z) == True{} : Bool}:
53  MNat.le_trans(x, y, z, xy, yz)