Interior Bisector

Textbook formulation:

Let A B C be a triangle with \(TraditionalForm\`AB\&_\) ≤ \(TraditionalForm\`AC\&_\) and AD the interior bisector of ∠BAC (D ∈BC). Prove that \(TraditionalForm\`BD\&_\) ≤ \(TraditionalForm\`DC\&_\).

Input to the system:

Proposition["Cad_bisect",  
      any[A, B, C, 
        D], 
point[ A, D, 
            B] ∧ 
bisectint[A, D, A, B, 
            C] ∧ 
hypothesis[
            seglengthsq[A, B] <= seglengthsq[A, C], 
            D]
 \[Implies] 
        inequation[seglengthsq[B, D] <= seglengthsq[D, C]]]

Input to the system:

Simplify[Proposition["Cad_bisect"], 
      by -> GraphicSimplifier]

Output generated automatically by the system

End of output

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

Inserted notebook generated automatically by the system

End of inserted notebook