def internal_sorted_tail_step

bend-mathlib@0.8.1.0 · list.bend:853

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

853def internal_sorted_tail_step(-x: Nat, +y: Nat, +t: List<&2, Nat>, b: Bool, e: {Nat.is_le(x, y) == b : Bool}, h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)) -> sorted_by(~Nat, ~Nat.is_le, y <> t):
854  match b:
855    case True{}:
856      Equal.trans(Bool, List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), (x, y) <> List.zip(&2, Nat, &2, Nat, y <> t, t)), True{}, internal_sorted_cons_true(~Nat, ~Nat.is_le, x, y, List.zip(&2, Nat, &2, Nat, y <> t, t), e), h)
857    case False{}:
858      Empty.absurd(sorted_by(~Nat, ~Nat.is_le, y <> t), MNat.internal_false_ne_true(Equal.trans(Bool, False{}, List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), (x, y) <> List.zip(&2, Nat, &2, Nat, y <> t, t)), True{}, internal_sorted_cons_false(~Nat, ~Nat.is_le, x, y, List.zip(&2, Nat, &2, Nat, y <> t, t), e), h)))