proposition: Fact list_an_duplicate_inv a n l x m y r : list_an a n = l++x::m++y::r -> a <= x /\ x < y < a+n.
proof: Proof. intros H. generalize H; intros H1. apply f_equal with (f := @length _) in H1. rewrite list_an_length in H1. apply list_an_app_inv in H; simpl in H. destruct H as (E1 & H); injection H; clear H; intros H E2. symmetry in H; apply list_an_app_inv in H; simpl in H. destruct H as (E3 & H); injection H; clear H; intros E4 E5. do 2 (rewrite app_length in H1; simpl in H1). lia. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)