proposition: Fact nat_list_insert_sorted x l : nat_sorted l -> nat_sorted (nat_list_insert x l).
proof: Proof. induction l as [ | y l IHl ]; simpl. intro; apply in_nat_sorted_1. intros H. generalize (Nat.ltb_lt x y) (Nat.ltb_lt y x). destruct (x <? y); destruct (y <? x); intros H1 H2. apply proj1 in H1; spec in H1; auto. apply proj1 in H2; spec in H2; auto. lia. apply in_nat_sorted_2; auto; tauto. apply in_nat_sorted_3. apply nat_list_insert_Forall. tauto. apply nat_sorted_Forall; auto. apply IHl; revert H; apply nat_sorted_cons_inv. auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)