proposition: Lemma qs_shift n m j k (v : vec nat k) : divides (qs n) (exp j v) <-> divides (qs (m + n)) (exp (m + j) v).
proof: Proof. revert m n j; induction v as [ | x k v IHv ]; intros m n j. - cbn; split; intros ? % divides_1_inv % not_qs_1; tauto. - cbn. split. + intros [ | ] % divides_mult_inv; auto. * destruct x. -- cbn in H; revert H. intros ? % divides_1_inv % not_qs_1; tauto. -- eapply divides_pow in H; auto. eapply primestream_divides in H as ->. cbn; do 2 apply divides_mult_r; apply divides_refl. * eapply divides_mult. rewrite IHv with (m := m) in H. rewrite <- plus_n_Sm in H; auto. + intros [ | ] % divides_mult_inv; auto. * destruct x. -- cbn in H; revert H. intros ? % divides_1_inv % not_qs_1; tauto. -- eapply divides_pow in H; auto. eapply primestream_divides in H. assert (n = j) by lia. subst. cbn; do 2 apply divides_mult_r; apply divides_refl. * eapply divides_mult. replace (S (m + j)) with (m + S j) in H by lia. rewrite <- 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)