def internal_sorted_skip
bend-mathlib@0.8.1.0 · list.bend:945
import bend-mathlib@0.8.1.0/list.bend as List
import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat
945def internal_sorted_skip(+x: Nat, +z: Nat, t: List<&2, Nat>, h: sorted_by(~Nat, ~Nat.is_le, x <> z <> t)) -> sorted_by(~Nat, ~Nat.is_le, x <> t):
946 match t:
947 case Nil{}:
948 {==}
949 case +w <> u:
950 +u = u
951 +h = h
952 sorted_cons_cons_intro(x, w, u, MNat.le_trans(x, z, w, sorted_cons_cons_elim_le(x, z, w <> u, h), sorted_cons_cons_elim_le(z, w, u, sorted_cons_cons_elim_tail(x, z, w <> u, h))), sorted_cons_cons_elim_tail(z, w, u, sorted_cons_cons_elim_tail(x, z, w <> u, h)))