proposition: Lemma prime_above m : { p | m < p /\ prime p }.
proof: Proof. destruct (prime_factor (n := fact m + 1)) as (p & ? & ?). - pose proof (lt_O_fact m); lia. - exists p; eauto. destruct (Nat.lt_ge_cases m p); eauto. eapply divides_plus_inv in H0. + eapply divides_1_inv in H0; subst. destruct H; lia. + eapply divides_fact. eapply prime_ge_2 in H; 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)