aboutsummaryrefslogtreecommitdiff
path: root/coqprime/examples/PocklingtonRefl.v
blob: 6b7a0e0c1e2796ba837d654292ba6053a2879f85 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14

(*************************************************************)
(*      This file is distributed under the terms of the      *)
(*      GNU Lesser General Public License Version 2.1        *)
(*************************************************************)
(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
(*************************************************************)

Require Export List.
Require Export ZArith.
Require Export Znumtheory.
Require Export Pock.
Require Export BasePrimes.