Library Coqprime.num.MEll

Require Import ZArith Znumtheory Zpow_facts.
Require Import Int31 ZEll montgomery.

Set Implicit Arguments.

Open Scope Z_scope.

Record ex: Set := mkEx {
  vN : positive;
  vS : positive;
  vR: List.list (positive * positive);
  vA: Z;
  vB: Z;
  vx: Z;
  vy: Z
}.

Local Coercion Zpos : positive >-> Z.

Record ex_spec (exx: ex): Prop := mkExS {
  n2_div: ~(2 | exx.(vN));
  n_pos: 2 < exx.(vN);
 lprime:
  forall p : positive * positive, List.In p (vR exx) -> prime (fst p);
   lbig:
    4 * vN exx < (Zmullp (vR exx) - 1) ^ 2;
   inC:
    vy exx ^ 2 mod vN exx = (vx exx ^ 3 + vA exx * vx exx + vB exx) mod vN exx
}.