fact: Fixpoint nat_list_insert x l := match l with | nil => x::nil | y::l => if x <? y then x::y::l else if y <? x then y::nat_list_insert x l else y::l end.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)