proposition: Fact exp_app n m i v w : @exp (n+m) i (vec_app v w) = exp i v * exp (n+i) w.
proof: Proof. revert i; induction v as [ | x n v IHv ]; intros i. + rewrite vec_app_nil, exp_zero; simpl; ring. + rewrite vec_app_cons, exp_cons. simpl plus; rewrite exp_cons, IHv. replace (n+S i) with (S (n+i)) by lia; ring. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)