def internal_sorted_least_head

bend-mathlib@0.8.1.0 · sort.bend:124

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

124def internal_sorted_least_head(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, +xs: List<&2, A>, +x: A, +h: MList.sorted_by(~A, ~le, x <> xs)) -> internal_least(~A, ~le, x, xs):
125  match xs:
126    case Nil{}:
127      {==}
128    case +y <> +t:
129      internal_least_intro(~A, ~le, x, y, t, internal_sorted_cons_cons_elim_le(~A, ~le, x, y, t, h), internal_least_trans(~A, ~le, ~le_trans, x, y, t, internal_sorted_cons_cons_elim_le(~A, ~le, x, y, t, h), internal_sorted_least_head(~A, ~le, ~le_trans, t, y, internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h))))