;;
;; Prove Apollonius circle theorem
;;
(prove-theorem
 ((perpendicular A B A C)
  (midpoint B C M)
  (midpoint A M O)
  (collinear B H C)
  (perpendicular A H B C))
 ((equidistant M O H O)
  (identical-points B C)
  ))