proposition: Fact nat_sort_length l : length (nat_sort l) <= length l.
proof: Proof. induction l as [ | x l IHl ]; simpl. lia. apply Nat.le_trans with (1 := nat_list_insert_length _ _); lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)