Challenge: exclude rational points of order twenty-five

theorem MazurTheorem.Challenge.no_rational_point_of_order_twentyFive (E : WeierstrassCurve ℚ) [E.IsElliptic] (P : (WeierstrassCurve.Affine.baseChange E ℚ).Point) : addOrderOf P ≠ 25

An elliptic curve over the rationals has no rational point of exact additive order twenty-five.