proposition: Fact exp_cons n i x v : @exp (S n) i (x##v) = qs i^x*exp (S i) v.
proof: Proof. auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)