proposition: Fact in_nat_sorted_3 x ll : Forall (lt x) ll -> nat_sorted ll -> nat_sorted (x::ll).
proof: Proof. induction 1 as [ | y ll Hll IHl ]. intro; apply in_nat_sorted_1. intros H. apply in_nat_sorted_2; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)