proposition: Lemma qs_exp_div i j n v : i < j -> ~ divides (qs i) (@exp n j v).
proof: Proof. Proof with eauto. revert i j; induction v; intros i j Hi. + cbn; intros ? % divides_1_inv % not_qs_1; auto. + cbn; intros [ H % divides_pow | H ] % divides_mult_inv; eauto. * eapply primestream_divides in H; lia. * eapply IHv in H; 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)