src/Util/ZUtil/Tactics/PrimeBound.v


1
2
3
4
5
6
7

Require Import Coq.omega.Omega Coq.ZArith.Znumtheory.

Module Z.
  Ltac prime_bound := match goal with
  | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega
  end.
End Z.