Sort.internal_least_cons_tail: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/sort.bend as Sort
Lines 114-115 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=114&end_line=115

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

def internal_least_cons_tail(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: internal_least(~A, ~le, lo, h <> t)) -> internal_least(~A, ~le, lo, t):
  MList.internal_and_right(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_right
  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