1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15

import Mathlib

variable (a b c : ℂ)

def complexCollinear := ((a - b) / (b - c)).im = 0

-- Root of 3x^2-2(a+b+c)x+(ab+bc+ac)
noncomputable def derivPosRoot := (a + b + c + ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) ^ (1 / 2 : ℂ)) / 3

noncomputable def derivNegRoot := (a + b + c - ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) ^ (1 / 2 : ℂ)) / 3

noncomputable def distSum (z : ℂ) := ‖derivPosRoot a b c - z‖ + ‖derivNegRoot a b c - z‖

theorem marden (h : ¬complexCollinear a b c) : ∃ d, distSum (z := a / 2 + b / 2) = d ∧ distSum (z := b / 2 + c / 2) = d ∧ distSum (z := a / 2 + c / 2) = d := by
  sorry