law sorted_tail

bend-mathlib@0.8.1.0 · list.bend:886

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

import Base

886# The tail of a nonempty Nat list sorted by Nat.is_le is sorted.
887law sorted_tail:
888  for x: Nat
889  for xs: List<&2, Nat>
890  for h: sorted_by(~Nat, ~Nat.is_le, x <> xs)
891  sorted_by(~Nat, ~Nat.is_le, xs)

Uses (5)

Used by (2)