proposition: Lemma prime_dec p : { prime p } + { ~ prime p }.
proof: Proof. destruct (le_lt_dec 2 p) as [ H | H ]. + destruct (prime_or_div H) as [ (q & H1 & H2) | ? ]; auto. right; intros C; apply C in H2; lia. + right; intros (H1 & H2). destruct (H2 2); try lia. exists 0; simpl; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)