Library circumcenter

Require Export perp_bisect.

Section Circumcenter.

Context `{MT:Tarski_2D_euclidean}.
Context `{EqDec:EqDecidability Tpoint}.

Definition is_circumcenter G A B C := Cong A G B G ∧ Cong B G C G.

Lemma circumcenter_cong : ∀ G A B C,
 is_circumcenter G A B C →
 Cong A G B G ∧ Cong B G C G ∧ Cong C G A G.
Proof.
intros.
unfold is_circumcenter in ×.
intuition eCong.
Qed.

Lemma circumcenter_perp : ∀ A B C A' B' C' G,
  A≠B → B≠C → A≠C → G ≠ A' → G ≠ B' → G ≠ C' →
  is_circumcenter G A B C →
  is_midpoint A' B C →
  is_midpoint B' A C →
  is_midpoint C' A B →
  perp_bisect G A' B C ∧ perp_bisect G B' A C ∧ perp_bisect G C' A B.
Proof.
intros.
repeat split;
apply cong_perp_bisect;try assumption;
unfold is_midpoint, is_circumcenter in *;
intuition eCong.
Qed.

Lemma circumcenter_intersect : ∀ A B C A' B' C' G,
  A≠B → B≠C → A≠C → G ≠ A' → G ≠ B' → G ≠ C' →
  is_midpoint A' B C →
  is_midpoint B' A C →
  is_midpoint C' A B →
  perp_bisect G A' B C →
  perp_bisect G B' A C →
  Perp G C' A B.
Proof.
intros.
assert (is_circumcenter G A B C).
unfold is_circumcenter.
split.
assert (Cong A G C G).
apply (perp_bisect_cong G B' A C).
assumption.
assert (Cong B G C G).
apply (perp_bisect_cong G A' B C ).
assumption.
eCong.
apply (perp_bisect_cong G A' B C).
assumption.
assert (perp_bisect G C' A B).
assert (T:=circumcenter_perp A B C A' B' C' G ).
intuition.
auto with perp_bisect.
Qed.

End Circumcenter.