theorem Hex.ECPP.prime_order_dvd_card {G : Type u_1} [AddGroup G] [Fintype G] {q : ℕ} (hq : _root_.Nat.Prime q) {Q : G} (hne : Q ≠ 0) (hzero : q • Q = 0) : q ∣ Fintype.card G

A nonzero point annihilated by a prime has that order, which divides the cardinality of its finite group.

theorem Hex.ECPP.prime_order_le_card {G : Type u_1} [AddGroup G] [Fintype G] {q : ℕ} (hq : _root_.Nat.Prime q) {Q : G} (hne : Q ≠ 0) (hzero : q • Q = 0) : q ≤ Fintype.card G

A prime annihilating a nonzero point is at most the finite group order.

theorem Hex.ECPP.size_excludes_small_divisor (p n q N : ℕ) (hq2 : 2 ≤ q) (hsmall : p * p ≤ n) (horder : q ≤ N) (hhasse : (↑p + 1 - ↑N) ^ 2 ≤ 4 * ↑p) (hsize : sizeBound n q = true) : False

The strict ECPP size check rules out a prime divisor at most √n once its reduced curve has a point of order q.