proposition: Fact nxtprime_bool_spec n p : nxtprime_bool n p = true <-> nxtprime n = p.
proof: Proof. unfold nxtprime_bool. rewrite !andb_true_iff, Nat.leb_le, notprime_bool_rec_spec, prime_bool_spec. unfold nxtprime. destruct (first_prime_above n) as (q & G1 & G2 & G3); simpl. split. + intros ((H1 & H2) & H3). apply Nat.le_antisymm. * apply G3; auto. * apply Nat.nlt_ge. intro; apply (H2 q); auto; lia. + intros ->; lsplit 2; auto. intros q Hq C; apply G3 in C; 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)