fact: 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 }.
imports: ZArith Znumtheory Zpow_facts Uint63 ZEll montgomery