law sorted_take

bend-mathlib@0.8.1.0 · list.bend:912

import Base

912# A prefix of a Nat list sorted by Nat.is_le is sorted.
913law sorted_take:
914  for xs: List<&2, Nat>
915  for n: Nat
916  for h: sorted_by(~Nat, ~Nat.is_le, xs)
917  sorted_by(~Nat, ~Nat.is_le, List.take(&2, Nat, xs, n))