proposition: Fact nat_list_insert_Forall (P : nat -> Prop) x l : P x -> Forall P l -> Forall P (nat_list_insert x l).
proof: Proof. do 2 rewrite Forall_forall; intros H1 H2 y Hy. apply nat_list_insert_incl in Hy. destruct Hy; subst; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)