law sorted_drop

bend-mathlib@0.8.1.0 · list.bend:928

import Base

928# A suffix of a Nat list sorted by Nat.is_le is sorted.
929law sorted_drop:
930  for xs: List<&2, Nat>
931  for n: Nat
932  for h: sorted_by(~Nat, ~Nat.is_le, xs)
933  sorted_by(~Nat, ~Nat.is_le, List.drop(&2, Nat, xs, n))