def internal_head_le_mem

bend-mathlib@0.8.1.0 · list.bend:1001

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

1001def 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):
1002  match xs:
1003    case Nil{}:
1004      Empty.absurd(MNat.le(x, y), MNat.internal_false_ne_true(hm))
1005    case +z <> t:
1006      +x = x
1007      +y = y
1008      +t = t
1009      +hs = hs
1010      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))