law sorted_cons_cons_elim_tail

bend-mathlib@0.8.1.0 · list.bend:873

import bend-mathlib@0.8.1.0/list.bend as List

import Base

873# The tail of a Nat list of two or more elements sorted by Nat.is_le is sorted.
874law sorted_cons_cons_elim_tail:
875  for x: Nat
876  for y: Nat
877  for -t: List<&2, Nat>
878  for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
879  sorted_by(~Nat, ~Nat.is_le, y <> t)

Uses (15)

Used by (5)