theorem Hex.ECPP.hasse_sq_zmod (p : ℕ) [Fact (Nat.Prime p)] (W : WeierstrassCurve (ZMod p)) [WeierstrassCurve.IsElliptic W.toAffine] : (↑p + 1 - ↑(Fintype.card W.toAffine.Point)) ^ 2 ≤ 4 * ↑p

The restricted integer Hasse inequality over the prime fields used by ECPP. It holds in characteristics two and three as well, though ECPP checks exclude those characteristics before constructing its short curve.