List.internal_le_of_mem_step: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/list.bend as List
Lines 1024-1030 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=1024&end_line=1030

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

def internal_le_of_mem_step(+x: Nat, xs: List<&2, Nat>, +y: Nat, b: Bool, e: {Nat.is_eq(x, y) == b : Bool}, hs: sorted_by(~Nat, ~Nat.is_le, x <> xs), hm: {Bool.or(b, List.contains(~Nat, ~Nat.is_eq, xs, y)) == True{} : Bool}) -> MNat.le(x, y):
  match b:
    case True{}:
      %MNat.eq_of_is_eq(x, y, e) : MNat.le(x, _)
      MNat.le_refl(x)
    case False{}:
      sorted_head_le_mem(x, xs, y, hs, hm)

Uses (12):
  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=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=sorted_by
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=sorted_head_le_mem
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=eq_of_is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le_refl