proposition: Lemma ps_exp n m (v : vec nat m) i : ~ divides (ps n) (exp i v).
proof: Proof. revert i; induction v as [ | m x v IHv ]; intros i; simpl. - intros H % divides_1_inv; revert H; apply not_ps_1. - intros [H % divides_pow | ] % divides_mult_inv; eauto. + now eapply ps_qs_div in H. + eapply IHv; eauto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)