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

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

def internal_sorted_cons_of_least(~A: Data, ~le: A -> A -> Bool, +lo: A, +m: List<&2, A>, hl: internal_least(~A, ~le, lo, m), hm: MList.sorted_by(~A, ~le, m)) -> MList.sorted_by(~A, ~le, lo <> m):
  match m:
    case Nil{}:
      {==}
    case +z <> +t:
      internal_sorted_cons_cons_intro(~A, ~le, lo, z, t, internal_least_cons_le(~A, ~le, lo, z, t, hl), hm)

Uses (6):
  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=sorted_by
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_least
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_least_cons_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_sorted_cons_cons_intro