proposition: Lemma not_qs_1 n : ~ qs n = 1.
proof: Proof. intros H; generalize (str_prime qs n). rewrite H; apply not_prime_1. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)