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

;;
;; 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
 (
  (perpendicular A B A C) ; AB _|_ AC
  (midpoint B C M)        ; M is the midpoint of BC
  (midpoint A M O)        ; O is the midpoint of AM
  (collinear B H C)       ; H lies on BC
  (perpendicular A H B C) ; AH _|_ BC
  )
 ;; Then
 (
  (equidistant M O H O)   ; MO = HO
  ;; Or
  (identical-points B C)  ; B = C
  )
 )