proposition: Fact nat_list_insert_incl x l : incl (nat_list_insert x l) (x::l) /\ incl (x::l) (nat_list_insert x l).
proof: Proof. split. induction l as [ | y l IHl ]; simpl. intro; auto. destruct (x <? y); destruct (y <? x). intro; auto. intro; auto. intros ? [ [] | H ]; simpl; auto. apply IHl in H; simpl in H; tauto. intro; simpl; tauto. induction l as [ | y l IHl ]; simpl. intro; auto. generalize (Nat.ltb_lt x y) (Nat.ltb_lt y x). destruct (x <? y); destruct (y <? x); intros H1 H2 z; auto. intros [ Hz | [ Hz | Hz ] ]; subst. right; apply IHl; left; auto. left; auto. right; apply IHl; right; auto. destruct (lt_eq_lt_dec x y) as [ [ H | ] | H ]. apply H1 in H; discriminate. 2: apply H2 in H; discriminate. intros [ Hz | [ Hz | Hz ] ]; subst; auto. left; auto. left; auto. right; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)