proposition: Fact nat_sort_sorted l : nat_sorted (nat_sort l).
proof: Proof. induction l as [ | x l IHl ]. apply in_nat_sorted_0. simpl; apply nat_list_insert_sorted; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)