Some properties of a regular nonagon
In the figure a regular nonagon and a regular triangle ABO are given. J and K are midpoints of two neighbor sides of the nonagon. L is the midpoint of the nonagon, N is the midpoint of the arc AI of the circumcircle of the nonagon. Finally, M is the midpoint of the radius LN.
Prove that JM is parallel to OB. This is one formulation of Karst's statement.
GeoGebra can find an automatic proof by comparing JM and OB with the Relation tool. (As of August 2018 this statement cannot be completely proven with GeoGebra, just a numerical check can be performed.)