proposition: Fact in_nat_sorted_2 x y ll : x < y -> nat_sorted (y::ll) -> nat_sorted (x::y::ll).
proof: Proof. intros H1 H2 l a m b r H3. destruct l as [ | u l ]. inversion H3; subst. destruct m as [ | v m ]. inversion H4; subst; auto. inversion H4; subst. apply Nat.lt_trans with (1 := H1), (H2 nil _ m _ r); auto. inversion H3; subst. apply (H2 l _ m _ r); auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)