Sort.internal_least_cons_le: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/sort.bend as Sort
Lines 111-112 of bend-mathlib@0.8.1.0/sort.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/sort.bend&start_line=111&end_line=112

import Base
import bend-mathlib@0.8.1.0/list.bend as MList

def internal_least_cons_le(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: internal_least(~A, ~le, lo, h <> t)) -> {le(lo, h) == True{} : Bool}:
  MList.internal_and_left(le(lo, h), internal_all_ge(~A, ~le, lo, t), hh)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=internal_and_left
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_all_ge
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_least