proposition: Fact nat_sorted_Forall x ll : nat_sorted (x::ll) -> Forall (lt x) ll.
proof: Proof. rewrite Forall_forall; intros H y Hy. apply in_split in Hy. destruct Hy as (l & r & ?); subst. apply (H nil _ l _ r); auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)