proposition: Lemma exp_inj n i v1 v2 : @exp n i v1 = exp i v2 -> v1 = v2.
proof: Proof. revert i v2; induction v1 as [ | x n v1 IH ]; intros i v2. + vec nil v2; auto. + vec split v2 with y. simpl; intros H. assert (forall v, ~ divides (qs i) (@exp n (S i) v)) as G. { intros v; apply qs_exp_div; auto. } apply power_factor_uniq in H; auto. destruct H; f_equal; subst; 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)