proposition: Lemma qs_ps_div n m : ~ divides (qs n) (ps m).
proof: Proof. intros ? % prime_divides; 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)