proposition: Lemma first_prime_above m : { p | m < p /\ prime p /\ forall q, m < q -> prime q -> p <= q }.
proof: Proof. destruct min_dec with (P := fun p => m < p /\ prime p) as (p & H1 & H2). + intros n. destruct (lt_dec m n); destruct (prime_dec n); tauto. + destruct (prime_above m) as (p & ?); exists p; auto. + exists p; firstorder. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)