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

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

def internal_sorted_append_cons(t: List<&2, Nat>, ys: List<&2, Nat>, +x: Nat, bnd: @a: Nat -> @b: Nat -> mem(~Nat, ~Nat.is_eq, a, x <> t) -> mem(~Nat, ~Nat.is_eq, b, ys) -> MNat.le(a, b), hx: sorted_by(~Nat, ~Nat.is_le, x <> t), hy: sorted_by(~Nat, ~Nat.is_le, ys)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.append(&2, Nat, t, ys)):
  match t:
    case Nil{}:
      match ys:
        case Nil{}:
          {==}
        case +y <> u:
          +u = u
          sorted_cons_cons_intro(x, y, u, bnd(x, y, mem_cons_self(x, Nil{}), mem_cons_self(y, u)), hy)
    case +z <> u:
      +u = u
      +hx = hx
      sorted_cons_cons_intro(x, z, List.append(&2, Nat, u, ys), sorted_cons_cons_elim_le(x, z, u, hx), internal_sorted_append_cons(u, ys, z, +a => b => ma => mb => bnd(a, b, mem_cons_of_mem(a, x, z <> u, ma), mb), sorted_cons_cons_elim_tail(x, z, u, hx), hy))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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=mem
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=mem_cons_of_mem
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=mem_cons_self
  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/list.bend&name=sorted_cons_cons_intro
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=le