OG ≤ OI ≤ OH

Textbook formulation:

Let O be the circumcenter, I the incenter, G the centroid and H the orthocenter of a triangle. Then OG ≤ OI ≤ OH.

Input to the system:

Proposition["Cad_points",  
      any[II, A, B, C, P, H, M, N, O, 
        G], 
point[II, A, 
            B] ∧ 
incircle[II, A, B, C, 
            P] ∧ 
inter[H, 
            tline[ A, B, C], 
            tline[ B, A, C]] ∧ 
median[
            C, M, A, B, C] ∧ 
median[B, N, A, B, 
            C] ∧ 
inter[O, 
            tline[ M, A, B], 
            tline[ N, A, C]] ∧ 
          circle[O, A] ∧ 
inter[G, 
            line[ C, M], 
            line[ B, N]]
 \[Implies] 
        inequation[
            seglengthsq[O, H] - seglengthsq[O, II] >= 
              0] ∧ 
inequation[
            seglengthsq[O, II] - seglengthsq[O, G] >= 0]]

Input to the system:

KnowledgeBase["Cad_points_g", 
      any[A, B, 
        II], {{ A, {0, 
            0}}, {B, {-123, -123}}, {II, {-23, -75}}}]

Input to the system:

Simplify[Proposition["Cad_points"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Cad_points_g"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Cad_points"], by -> GeometryProver, 
      ProverOptions -> {Method -> "AreaCAD"}]

Inserted notebook generated automatically by the system

End of inserted notebook