fact: Fixpoint exp {n} (i : nat) (v : vec nat n) : nat := match v with | vec_nil => 1 | x##v => qs i ^ x * exp (S i) v end.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)