proposition: Fact nat_sorted_head_inv x y ll : nat_sorted (x::y::ll) -> x < y.
proof: Proof. intros H; apply (H nil _ nil _ ll); solve list eq. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)