law sorted_cons_cons_elim_le
import bend-mathlib@0.8.1.0/list.bend as Listimport Base
import bend-mathlib@0.8.1.0/nat.bend as MNat
860# The first two elements of a Nat list sorted by Nat.is_le are in order.
861law sorted_cons_cons_elim_le:
862 for x: Nat
863 for y: Nat
864 for -t: List<&2, Nat>
865 for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
866 MNat.le(x, y)