Incircle and Circumcircle

Textbook formulation:

Let ABC a triangle, r and R the radius of the incircle resp. circumcircle. Show that 2 r ≤ R and 9  (R^2) ≤ (a^2) + (b^2) + (c^2).

Input to the system:

Proposition["Cad_incircle",  
      any[O, A, B, C, P, X, Y, 
        O1], 
point[O, A, 
            B] ∧ 
incircle[O, A, B, C, 
            P] ∧ 
midpoint[ X, A, 
            B] ∧ 
midpoint[ Y, A, 
            C] ∧ 
          inter[O1, tline[ X, A, B], 
            tline[ Y, A, C]] ∧ 
circle[
            O1, A]
 \[Implies] 
        inequation[4*seglengthsq[O, P] <= seglengthsq[O1, A]] ∧ 
          inequation[
            9*seglengthsq[O1, A] >= 
              seglengthsq[A, B] + seglengthsq[A, C] + 
                seglengthsq[B, C]]]

Input to the system:

KnowledgeBase["Cad_incircle_g", 
      any[A, B, 
        O], {{ A, {0, 
            0}}, {B, {-123, -123}}, {O, {-23, -75}}}]

Input to the system:

Simplify[Proposition["Cad_incircle"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Cad_incircle_g"]]

Output generated automatically by the system

End of output

Input to the system:

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

Inserted notebook generated automatically by the system

End of inserted notebook