;; Prove Desargues Theorem.
;;
;; Desargues Theorem (Wikipedia): In a projective space, two triangles
;; are in perspective axially if and only if they are in perspective
;; centrally.

(translate-theorem
 (
  ;; If

  ;; Triangles are in perspective centrally
  ;; O is the center of projectivity
  (collinear A0 A1 O)
  (collinear B0 B1 O)
  (collinear C0 C1 O)

  ;; and X, Y, Z are points on the axis of projectivity
  (collinear A0 C0 Y)
  (collinear B0 C0 X)
  (collinear A0 B0 Z)

  (collinear A1 C1 Y)
  (collinear B1 C1 X)
  (collinear A1 B1 Z)
  )
 ;; Then
 ((collinear X Y Z)

  ;; What if X Y X are at infinity?
  ;; Or one of the triangles is degenerate?

  ;;(identical-points A0 C0)
  ;;(identical-points A0 B0)
  ;;(identical-points B0 C0)

  ;;(identical-points A1 C1)
  ;;(identical-points A1 B1)
  ;;(identical-points B1 C1)

  )
 ;; :order #'grlex>
 )