proposition: Fact nat_list_insert_length x l : length (nat_list_insert x l) <= S (length l).
proof: Proof. induction l as [ | y l IHl ]; simpl. lia. destruct (x <? y); simpl; try lia. destruct (y <? x); simpl; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)