proposition: Fact list_an_app_inv a n l r : list_an a n = l++r -> l = list_an a (length l) /\ r = list_an (a+length l) (length r).
proof: Proof. revert a l r; induction n as [ | n IHn ]; intros a l r; simpl. + destruct l; destruct r; intros; auto; discriminate. + destruct l as [ | x l ]; simpl; intros H1. * split; auto. rewrite <- H1; simpl; rewrite Nat.add_0_r, list_an_length; auto. * injection H1; clear H1; intros H1 H0. apply IHn in H1; destruct H1; split; f_equal; auto. rewrite H1 at 1; f_equal; lia. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)