Challenge: exclude rational points of order thirty-five

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

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