List.internal_head_le_mem: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/list.bend as List
Lines 1001-1010 of bend-mathlib@0.8.1.0/list.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/list.bend&start_line=1001&end_line=1010

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

def internal_head_le_mem(xs: List<&2, Nat>, x: Nat, y: Nat, hs: sorted_by(~Nat, ~Nat.is_le, x <> xs), hm: mem(~Nat, ~Nat.is_eq, y, xs)) -> MNat.le(x, y):
  match xs:
    case Nil{}:
      Empty.absurd(MNat.le(x, y), MNat.internal_false_ne_true(hm))
    case +z <> t:
      +x = x
      +y = y
      +t = t
      +hs = hs
      internal_head_le_mem_step(x, z, t, y, Nat.is_eq(z, y), {==}, sorted_cons_cons_elim_le(x, z, t, hs), Equal.trans(Bool, Bool.or(Nat.is_eq(z, y), List.contains(~Nat, ~Nat.is_eq, t, y)), List.contains(~Nat, ~Nat.is_eq, z <> t, y), True{}, internal_contains_cons(~Nat, ~Nat.is_eq, z, t, y), hm), k => internal_head_le_mem(t, z, y, sorted_cons_cons_elim_tail(x, z, t, hs), k))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.contains
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=internal_contains_cons
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=internal_head_le_mem_step
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=mem
  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/list.bend&name=sorted_cons_cons_elim_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=sorted_cons_cons_elim_tail
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=internal_false_ne_true
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le