def internal_sorted_cons_of_least

bend-mathlib@0.8.1.0 · sort.bend:131

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

131def 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):
132  match m:
133    case Nil{}:
134      {==}
135    case +z <> +t:
136      internal_sorted_cons_cons_intro(~A, ~le, lo, z, t, internal_least_cons_le(~A, ~le, lo, z, t, hl), hm)