law sorted_cons_cons_intro
import bend-mathlib@0.8.1.0/list.bend as Listimport Base
import bend-mathlib@0.8.1.0/nat.bend as MNat
840# A Nat list sorted by Nat.is_le stays sorted under a head that is <= the next element.
841law sorted_cons_cons_intro:
842 for -x: Nat
843 for -y: Nat
844 for -t: List<&2, Nat>
845 for hxy: MNat.le(x, y)
846 for hyt: sorted_by(~Nat, ~Nat.is_le, y <> t)
847 sorted_by(~Nat, ~Nat.is_le, x <> y <> t)