source: CGBLisp/trunk/examples/prover-apollonius.lisp@ 99

;;
;; Prove Apollonius Circle Theorem:
;;----------------------------------------------------------------
;; If ABC is a right triangle with hypotenuse BC,
;; and
;;
;; 1) M is the midpoint of BC;
;; 2) M1 is the midpoint of AB;
;; 3) M2 is the midpoint of AC;
;; 4) is the foot of the altitude dropped from A;
;;
;; then A, H, M1, M2 and M lie on the same circle.
;;----------------------------------------------------------------
;;

(prove-theorem

 ;; If
 (
  ;; AB _|_ AC
  (perpendicular A B A C)

  ;; M is the midpoint of BC
  (midpoint B C M)

  ;; O is the midpoint of AM
  (midpoint A M O)

  ;; H lies on BC
  (collinear B H C)

  ;; AH _|_ BC
  (perpendicular A H B C)

  )

 ;; Then

 (
  ;; MO = HO
  (equidistant M O H O)

  ;; or

  ;; B = C
  (identical-points B C)

  )
 )