proposition: Fact list_an_plus a n m : list_an a (n+m) = list_an a n ++ list_an (n+a) m.
proof: Proof. revert a; induction n; intros a; simpl; auto. rewrite IHn; do 3 f_equal; lia. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)