proposition: Fact nat_sort_eq l : incl (nat_sort l) l /\ incl l (nat_sort l).
proof: Proof. induction l as [ | x l IHl ]; simpl; split; intros y Hy; auto. apply nat_list_insert_incl in Hy; simpl. destruct Hy as [ | Hy ]; auto; right; apply IHl; auto. apply nat_list_insert_incl. destruct Hy; [ left | right ]; auto. apply IHl; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)