Library GeoCoq.Highschool.circumcenter
Require Export GeoCoq.Highschool.midpoint_thales.
Require Import GeoCoq.Highschool.exercises.
Section Circumcenter.
Context `{T2D:Tarski_2D}.
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 is_circumcenter_cases :
∀ A B C G,
is_circumcenter G A B C ∨
is_circumcenter G A C B ∨
is_circumcenter G B A C ∨
is_circumcenter G B C A ∨
is_circumcenter G C A B ∨
is_circumcenter G C B A →
is_circumcenter G A B C.
Proof.
intros.
decompose [or] H;clear H;
unfold is_circumcenter in *;spliter;
repeat (split; finish);eauto using cong_transitivity with cong.
Qed.
Lemma is_circumcenter_perm : ∀ A B C G,
is_circumcenter G A B C →
is_circumcenter G A B C ∧ is_circumcenter G A C B ∧
is_circumcenter G B A C ∧ is_circumcenter G B C A ∧
is_circumcenter G C A B ∧ is_circumcenter G C B A.
Proof.
intros.
apply circumcenter_cong in H.
spliter.
repeat split;Cong.
Qed.
Lemma is_circumcenter_perm_1 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G A C B.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
Lemma is_circumcenter_perm_2 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G B A C.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
Lemma is_circumcenter_perm_3 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G B C A.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
Lemma is_circumcenter_perm_4 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G C A B.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
Lemma is_circumcenter_perm_5 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G C B A.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
End Circumcenter.
Hint Resolve
is_circumcenter_perm_1
is_circumcenter_perm_2
is_circumcenter_perm_3
is_circumcenter_perm_4
is_circumcenter_perm_5 : Circumcenter.
Section Circumcenter2 .
Context `{TE:Tarski_2D_euclidean}.
Require Import GeoCoq.Highschool.exercises.
Section Circumcenter.
Context `{T2D:Tarski_2D}.
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 is_circumcenter_cases :
∀ A B C G,
is_circumcenter G A B C ∨
is_circumcenter G A C B ∨
is_circumcenter G B A C ∨
is_circumcenter G B C A ∨
is_circumcenter G C A B ∨
is_circumcenter G C B A →
is_circumcenter G A B C.
Proof.
intros.
decompose [or] H;clear H;
unfold is_circumcenter in *;spliter;
repeat (split; finish);eauto using cong_transitivity with cong.
Qed.
Lemma is_circumcenter_perm : ∀ A B C G,
is_circumcenter G A B C →
is_circumcenter G A B C ∧ is_circumcenter G A C B ∧
is_circumcenter G B A C ∧ is_circumcenter G B C A ∧
is_circumcenter G C A B ∧ is_circumcenter G C B A.
Proof.
intros.
apply circumcenter_cong in H.
spliter.
repeat split;Cong.
Qed.
Lemma is_circumcenter_perm_1 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G A C B.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
Lemma is_circumcenter_perm_2 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G B A C.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
Lemma is_circumcenter_perm_3 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G B C A.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
Lemma is_circumcenter_perm_4 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G C A B.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
Lemma is_circumcenter_perm_5 : ∀ A B C G,
is_circumcenter G A B C → is_circumcenter G C B A.
Proof.
intros.
apply is_circumcenter_perm in H;intuition.
Qed.
End Circumcenter.
Hint Resolve
is_circumcenter_perm_1
is_circumcenter_perm_2
is_circumcenter_perm_3
is_circumcenter_perm_4
is_circumcenter_perm_5 : Circumcenter.
Section Circumcenter2 .
Context `{TE:Tarski_2D_euclidean}.
Lemma circumcenter_perp : ∀ A B C A' G,
A≠B → B≠C → A≠C → G ≠ A' →
is_circumcenter G A B C →
Midpoint A' B C →
Perp_bisect G A' B C.
Proof.
intros.
apply cong_perp_bisect;try assumption;
unfold Midpoint, is_circumcenter in *;
intuition eCong.
Qed.
Lemma exists_circumcenter : ∀ A B C,
¬ Col A B C → ∃ G, is_circumcenter G A B C.
Proof.
intros.
assert (triangle_circumscription_principle).
apply (inter_dec_plus_par_perp_perp_imply_triangle_circumscription).
apply inter_dec.
unfold perpendicular_transversal_postulate.
apply par_perp_perp.
unfold triangle_circumscription_principle in ×.
destruct (H0 A B C H) as [G HG].
∃ G.
unfold is_circumcenter.
spliter.
split;eCong.
Qed.
Lemma circumcenter_perp_all : ∀ 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 →
Midpoint A' B C →
Midpoint B' A C →
Midpoint C' A B →
Perp_bisect G A' B C ∧ Perp_bisect G B' A C ∧ Perp_bisect G C' A B.
Proof.
intros.
split; try apply cong_perp_bisect; try (split; try apply cong_perp_bisect);
try assumption;
unfold 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' →
Midpoint A' B C →
Midpoint B' A C →
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_all A B C A' B' C' G ).
intuition.
eauto with Perp_bisect.
Qed.
Lemma is_circumcenter_uniqueness :
∀ A B C O O',
A≠B → B≠C → A≠C →
is_circumcenter O A B C →
is_circumcenter O' A B C →
O = O'.
Proof.
intros A B C O O' HAB HBC HAC HIC1 HIC2.
elim (Col_dec A B C); intro HABC.
{
Name C' the midpoint of A and B.
assert (HPer1 : Perp_bisect O C' A B).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; Cong.
intro; treat_equalities; assert (HFalse := l7_20 O B C); elim HFalse; clear HFalse;
try intro HFalse; Cong; assert_cols; try ColR.
apply HAC; apply symmetric_point_uniqueness with B O; Col; split; Between; Cong.
}
Name A' the midpoint of B and C.
assert (HPer2 : Perp_bisect O A' B C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; Cong.
intro; treat_equalities; assert (HFalse := l7_20 O A B); elim HFalse; clear HFalse;
try intro HFalse; Cong; assert_cols; try ColR.
apply HAC; apply symmetric_point_uniqueness with B O;
unfold Midpoint in*; spliter; split; Between; Cong.
}
assert (HPar : Par_strict O A' O C').
{
apply par_not_col_strict with C'; Col.
{
apply l12_9 with A B; try (apply perp_bisect_perp; assumption); Col.
apply perp_col0 with B C; Col; apply perp_sym; apply perp_bisect_perp; Col.
}
{
show_distinct A' C'; try (apply HAC; apply symmetric_point_uniqueness with B A';
unfold Midpoint in *; spliter; split; Cong; Between).
intro; assert (HFalse := l7_20 O A B); elim HFalse; clear HFalse; try intro HFalse;
unfold is_circumcenter in *; spliter; Cong; assert_diffs; assert_cols; try ColR.
assert (HOC' : O ≠ C').
{
apply perp_bisect_equiv_def in HPer1.
apply perp_bisect_equiv_def in HPer2.
unfold Perp_bisect in *; unfold Perp_at in *;
destruct HPer1 as [I [HOC' Hc1]]; assert_diffs; Col.
}
apply HOC'; apply l7_17 with A B; Col.
}
}
assert (HFalse := not_par_strict_id O A' C'); exfalso; apply HFalse; Col.
}
{
Name C' the midpoint of A and B.
elim (eq_dec_points O C'); intro HOC'; elim (eq_dec_points O' C'); intro HO'C';
treat_equalities; Col.
{
assert (HPer : Per A C B).
{
apply midpoint_thales with O; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
Name B' the midpoint of A and C.
assert (HO'B' : O' ≠ B').
{
intro; treat_equalities.
assert (HPer2 : Per A B C).
{
apply midpoint_thales with O'; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
assert (HPar : Par_strict A B A C).
{
apply par_not_col_strict with C; Col.
apply l12_9 with B C; Col;
try apply per_perp; Col; apply perp_right_comm; apply per_perp; Col.
}
assert (HFalse := not_par_strict_id A B C); exfalso; apply HFalse; Col.
}
Name A' the midpoint of B and C.
assert (HO'A' : O' ≠ A').
{
intro; treat_equalities.
assert (HPer2 : Per B A C).
{
apply midpoint_thales with O'; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
assert (HPar : Par_strict B A B C).
{
apply par_not_col_strict with C; Col.
apply l12_9 with A C; Col;
try apply per_perp; Col; apply perp_right_comm; apply per_perp; Perp.
}
assert (HFalse := not_par_strict_id B A C); exfalso; apply HFalse; Col.
}
assert (H : Perp_bisect O' A' B C ∧ Perp_bisect O' B' A C ∧ Perp_bisect O' O A B).
{
apply circumcenter_perp_all; Col.
}
destruct H as [HPer3 [HPer4 Hc]]; clear Hc.
assert (HPer1 : Perp_bisect O A' B C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; Cong.
show_distinct O B; Col.
intro; treat_equalities; apply HABC; assert_cols; ColR.
}
assert (HPer2 : Perp_bisect O B' A C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; eCong.
show_distinct O A; Col.
intro; treat_equalities; apply HABC; assert_cols; ColR.
}
apply l6_21 with O A' B' O'; Col.
{
assert (HRect : Rectangle C B' O A').
{
apply Per_mid_rectangle with B A; Perp; unfold Midpoint in *; spliter;
split; Between; Cong.
}
destruct HRect as [HPara Hc]; clear Hc.
apply plg_to_parallelogram in HPara.
apply plg_permut in HPara.
intro HOA'B'; apply plg_col_plgf in HPara; Col.
destruct HPara as [Hc1 [HCol2 Hc2]]; clear Hc1; clear Hc2.
assert_diffs; assert_cols; apply HABC; ColR.
}
{
apply col_permutation_2; apply perp_perp_col with B C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
{
apply col_permutation_5; apply perp_perp_col with A C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
}
{
assert (HPer : Per A C B).
{
apply midpoint_thales with O'; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
Name B' the midpoint of A and C.
assert (HOB' : O ≠ B').
{
intro; treat_equalities.
assert (HPer2 : Per A B C).
{
apply midpoint_thales with O; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
assert (HPar : Par_strict A B A C).
{
apply par_not_col_strict with C; Col.
apply l12_9 with B C; Col;
try apply per_perp; Col; apply perp_right_comm; apply per_perp; Col.
}
assert (HFalse := not_par_strict_id A B C); exfalso; apply HFalse; Col.
}
Name A' the midpoint of B and C.
assert (HOA' : O ≠ A').
{
intro; treat_equalities.
assert (HPer2 : Per B A C).
{
apply midpoint_thales with O; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
assert (HPar : Par_strict B A B C).
{
apply par_not_col_strict with C; Col.
apply l12_9 with A C; Col;
try apply per_perp; Col; apply perp_right_comm; apply per_perp; Perp.
}
assert (HFalse := not_par_strict_id B A C); exfalso; apply HFalse; Col.
}
assert (H : Perp_bisect O A' B C ∧ Perp_bisect O B' A C ∧ Perp_bisect O O' A B).
{
apply circumcenter_perp_all; Col.
}
destruct H as [HPer3 [HPer4 Hc]]; clear Hc.
assert (HPer1 : Perp_bisect O' A' B C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; Cong.
show_distinct O' B; Col.
intro; treat_equalities; apply HABC; assert_cols; ColR.
}
assert (HPer2 : Perp_bisect O' B' A C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; eCong.
show_distinct O' A; Col.
intro; treat_equalities; apply HABC; assert_cols; ColR.
}
apply l6_21 with O' A' B' O; Col.
{
assert (HRect : Rectangle C B' O' A').
{
apply Per_mid_rectangle with B A; Perp; unfold Midpoint in *; spliter;
split; Between; Cong.
}
destruct HRect as [HPara Hc]; clear Hc.
apply plg_to_parallelogram in HPara.
apply plg_permut in HPara.
intro HO'A'B'; apply plg_col_plgf in HPara; Col.
destruct HPara as [Hc1 [HCol2 Hc2]]; clear Hc1; clear Hc2.
assert_diffs; assert_cols; apply HABC; ColR.
}
{
apply col_permutation_2; apply perp_perp_col with B C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
{
apply col_permutation_5; apply perp_perp_col with A C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
}
{
Name B' the midpoint of A and C.
elim (eq_dec_points O B'); intro HOB'; elim (eq_dec_points O' B'); intro HO'B';
treat_equalities; Col.
{
assert (HPer : Per A B C).
{
apply midpoint_thales with O; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
Name A' the midpoint of B and C.
assert (HO'A' : O' ≠ A').
{
intro; treat_equalities.
assert (HPer2 : Per B A C).
{
apply midpoint_thales with O'; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
assert (HPar : Par_strict A C B C).
{
apply par_not_col_strict with B; Col.
apply l12_9 with A B; Col;
try (apply perp_left_comm; apply per_perp; Perp);
try (apply perp_comm; apply per_perp; Perp).
}
assert (HFalse := not_par_strict_id C A B); exfalso; apply HFalse; Par.
}
assert (H : Perp_bisect O' A' B C ∧ Perp_bisect O' O A C ∧ Perp_bisect O' C' A B).
{
apply circumcenter_perp_all; Col.
}
destruct H as [HPer3 [Hc HPer4]]; clear Hc.
assert (HPer1 : Perp_bisect O A' B C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; Cong.
show_distinct O C; Col.
intro; treat_equalities; apply HABC; assert_cols; ColR.
}
assert (HPer2 : Perp_bisect O C' A B).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; eCong.
}
apply l6_21 with O A' C' O'; Col.
{
assert (HRect : Rectangle B A' O C').
{
apply Per_mid_rectangle with A C; Perp; unfold Midpoint in *; spliter;
split; Between; Cong.
}
destruct HRect as [HPara Hc]; clear Hc.
apply plg_to_parallelogram in HPara.
apply plg_permut in HPara.
intro HOA'C'; apply plg_col_plgf in HPara; Col.
destruct HPara as [Hc1 [HCol2 Hc2]]; clear Hc1; clear Hc2.
assert_diffs; assert_cols; apply HABC; ColR.
}
{
apply col_permutation_2; apply perp_perp_col with B C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
{
apply col_permutation_5; apply perp_perp_col with A B; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
}
{
assert (HPer : Per A B C).
{
apply midpoint_thales with O'; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
Name A' the midpoint of B and C.
assert (HOA' : O ≠ A').
{
intro; treat_equalities.
assert (HPer2 : Per B A C).
{
apply midpoint_thales with O; unfold is_circumcenter in *;
spliter; Col; try split; eCong.
}
assert (HPar : Par_strict A C B C).
{
apply par_not_col_strict with B; Col.
apply l12_9 with A B; Col;
try (apply perp_left_comm; apply per_perp; Perp);
try (apply perp_comm; apply per_perp; Perp).
}
assert (HFalse := not_par_strict_id C A B); exfalso; apply HFalse; Par.
}
assert (H : Perp_bisect O A' B C ∧ Perp_bisect O O' A C ∧ Perp_bisect O C' A B).
{
apply circumcenter_perp_all; Col.
}
destruct H as [HPer3 [Hc HPer4]]; clear Hc.
assert (HPer1 : Perp_bisect O' A' B C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; Cong.
show_distinct O' C; Col.
intro; treat_equalities; apply HABC; assert_cols; ColR.
}
assert (HPer2 : Perp_bisect O' C' A B).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; eCong.
}
apply l6_21 with O' A' C' O; Col.
{
assert (HRect : Rectangle B A' O' C').
{
apply Per_mid_rectangle with A C; Perp; unfold Midpoint in *; spliter;
split; Between; Cong.
}
destruct HRect as [HPara Hc]; clear Hc.
apply plg_to_parallelogram in HPara.
apply plg_permut in HPara.
intro HO'A'C'; apply plg_col_plgf in HPara; Col.
destruct HPara as [Hc1 [HCol2 Hc2]]; clear Hc1; clear Hc2.
assert_diffs; assert_cols; apply HABC; ColR.
}
{
apply col_permutation_2; apply perp_perp_col with B C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
{
apply col_permutation_5; apply perp_perp_col with A B; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
}
{
Name A' the midpoint of B and C.
elim (eq_dec_points O A'); intro HOA'; elim (eq_dec_points O' A'); intro HO'A';
treat_equalities; Col.
{
assert (HPer : Per C A B).
{
apply midpoint_thales with O; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; Col; try split; eCong; Between.
}
assert (H : Perp_bisect O' O B C ∧ Perp_bisect O' B' A C ∧ Perp_bisect O' C' A B).
{
apply circumcenter_perp_all; Col.
}
destruct H as [Hc [HPer3 HPer4]]; clear Hc.
assert (HPer1 : Perp_bisect O B' A C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; eCong.
}
assert (HPer2 : Perp_bisect O C' A B).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; eCong.
}
apply l6_21 with O B' C' O'; Col.
{
assert (HRect : Rectangle A B' O C').
{
apply Per_mid_rectangle with B C; Perp; unfold Midpoint in *; spliter;
split; Between; Cong.
}
destruct HRect as [HPara Hc]; clear Hc.
apply plg_to_parallelogram in HPara.
apply plg_permut in HPara.
intro HOB'C'; apply plg_col_plgf in HPara; Col.
destruct HPara as [Hc1 [HCol2 Hc2]]; clear Hc1; clear Hc2.
assert_diffs; assert_cols; apply HABC; ColR.
}
{
apply col_permutation_2; apply perp_perp_col with A C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
{
apply col_permutation_5; apply perp_perp_col with A B; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
}
{
assert (HPer : Per C A B).
{
apply midpoint_thales with O'; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; Col; try split; eCong; Between.
}
assert (H : Perp_bisect O O' B C ∧ Perp_bisect O B' A C ∧ Perp_bisect O C' A B).
{
apply circumcenter_perp_all; Col.
}
destruct H as [Hc [HPer3 HPer4]]; clear Hc.
assert (HPer1 : Perp_bisect O' B' A C).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; eCong.
}
assert (HPer2 : Perp_bisect O' C' A B).
{
apply cong_perp_bisect; unfold is_circumcenter in *;
unfold Midpoint in *; spliter; eCong.
}
apply l6_21 with O' B' C' O; Col.
{
assert (HRect : Rectangle A B' O' C').
{
apply Per_mid_rectangle with B C; Perp; unfold Midpoint in *; spliter;
split; Between; Cong.
}
destruct HRect as [HPara Hc]; clear Hc.
apply plg_to_parallelogram in HPara.
apply plg_permut in HPara.
intro HO'B'C'; apply plg_col_plgf in HPara; Col.
destruct HPara as [Hc1 [HCol2 Hc2]]; clear Hc1; clear Hc2.
assert_diffs; assert_cols; apply HABC; ColR.
}
{
apply col_permutation_2; apply perp_perp_col with A C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
{
apply col_permutation_5; apply perp_perp_col with A B; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
}
{
assert (H : Perp_bisect O A' B C ∧ Perp_bisect O B' A C ∧ Perp_bisect O C' A B).
{
apply circumcenter_perp_all; Col.
}
destruct H as [HPer1 [HPer2 Hc]]; clear Hc.
assert (H : Perp_bisect O' A' B C ∧ Perp_bisect O' B' A C ∧ Perp_bisect O' C' A B).
{
apply circumcenter_perp_all; Col.
}
destruct H as [HPer3 [HPer4 Hc]]; clear Hc.
apply l6_21 with O A' B' O; Col.
{
intro HOA'B'; assert (HPar : Par_strict A C C B).
{
apply par_not_col_strict with B; Col.
apply l12_9 with O A'; Col;
try (apply perp_col0 with O B'; Col; apply perp_bisect_perp; assumption);
apply perp_sym; apply perp_right_comm; apply perp_bisect_perp; Col.
}
assert (HFalse := not_par_strict_id C A B); apply HFalse; Par.
}
{
apply col_permutation_2; apply perp_perp_col with B C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
{
apply col_permutation_5; apply perp_perp_col with A C; apply perp_bisect_perp;
apply perp_bisect_sym_1; Col.
}
}
}
}
}
Qed.
End Circumcenter2.
Section Circumcenter3.
Context `{TE:Tarski_2D_euclidean}.
Lemma midpoint_thales_reci_circum :
∀ A B C O: Tpoint,
Per A C B →
Midpoint O A B →
is_circumcenter O A B C.
Proof.
intros.
assert (T:= midpoint_thales_reci A B C O H H0).
spliter.
split;finish.
Qed.
Lemma circumcenter_per :
∀ A B C O,
A≠B → B≠C →
Per A B C →
is_circumcenter O A B C →
Midpoint O A C.
Proof.
intros.
Name O' the midpoint of A and C.
assert (T:= midpoint_thales_reci_circum A C B O' H1 H4).
assert (O=O').
apply is_circumcenter_uniqueness with A B C;finish.
intro.
treat_equalities.
apply l8_8 in H1.
intuition.
auto using is_circumcenter_perm_1.
subst;auto.
Qed.
End Circumcenter3.