proposition: Lemma is_circumcenter_uniqueness : forall 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: 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). { unfold is_circumcenter in *; spliter; apply cong_mid_perp_bisect; Cong. intro; treat_equalities; assert (HFalse := l7_20 O B C). destruct HFalse; Cong. ColR. treat_equalities; auto. } Name A' the midpoint of B and C. assert (HPer2 : Perp_bisect O A' B C). { unfold is_circumcenter in *; spliter; apply cong_mid_perp_bisect; Cong. intro; treat_equalities; assert (HFalse := l7_20 O A B). destruct HFalse; Cong. ColR. treat_equalities; auto. } assert (HPar : Par_strict O A' O C'). { apply par_not_col_strict with C'; Col. { apply l12_9 with A B; [Cop..| |Cop| |apply perp_bisect_perp; assumption]. apply col__coplanar; ColR. apply perp_col0 with B C; 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; Col. apply circumcenter_cong in HIC1; spliter; Cong. } 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'; Col. unfold is_circumcenter in *; spliter; Cong. } assert (HPar : Par_strict A B A C). { apply par_not_col_strict with C; Col. apply l12_9 with B C; [Cop..| |apply perp_right_comm]; apply per_perp; Perp. } 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'; Col. unfold is_circumcenter in *; spliter; Cong. } assert (HPar : Par_strict B A B C). { apply par_not_col_strict with C; Col. apply l12_9 with A C; [Cop..| |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). { unfold is_circumcenter in *; spliter. apply cong_mid_perp_bisect; Cong. intro; treat_equalities; apply HABC; Col. } assert (HPer2 : Perp_bisect O B' A C). { apply circumcenter_cong in HIC1; spliter. apply cong_mid_perp_bisect; Cong. intro; treat_equalities; apply HABC; Col. } 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, cop_perp2__col with B C; Perp; CopR. } { apply col_permutation_5, cop_perp2__col with A C; Perp; CopR. } } { assert (HPer : Per A C B). { apply midpoint_thales with O'; Col. apply circumcenter_cong in HIC2; spliter; Cong. } 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; Col. unfold is_circumcenter in *; spliter; Cong. } assert (HPar : Par_strict A B A C). { apply par_not_col_strict with C; Col. apply l12_9 with B C; [Cop..| |apply perp_right_comm]; apply per_perp; Perp. } 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; Col. unfold is_circumcenter in *; spliter; Cong. } assert (HPar : Par_strict B A B C). { apply par_not_col_strict with C; Col. apply l12_9 with A C; [Cop..| |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). { unfold is_circumcenter in *; spliter. apply cong_mid_perp_bisect; Cong. intro; treat_equalities; apply HABC; Col. } assert (HPer2 : Perp_bisect O' B' A C). { apply circumcenter_cong in HIC2; spliter. apply cong_mid_perp_bisect; Cong. intro; treat_equalities; apply HABC; Col. } apply l6_21 with O' A' B' O; Col. { assert (HRect : Rectangle C B' O' A'). { apply Per_mid_rectangle with B A; Perp; 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, cop_perp2__col with B C; Perp; CopR. } { apply col_permutation_5, cop_perp2__col with A C; Perp; CopR. } } { 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; Col. unfold is_circumcenter in *; spliter; Cong. } 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'; Col. unfold is_circumcenter in *; spliter; Cong. } assert (HPar : Par_strict A C B C). { apply par_not_col_strict with B; Col. apply l12_9 with A B; [Cop..|apply perp_left_comm|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). { unfold is_circumcenter in *; spliter. apply cong_mid_perp_bisect; Cong. intro; treat_equalities; apply HABC; Col. } assert (HPer2 : Perp_bisect O C' A B). { unfold is_circumcenter in *; spliter. apply cong_mid_perp_bisect; Cong. } apply l6_21 with O A' C' O'; Col. { assert (HRect : Rectangle B A' O C'). { apply Per_mid_rectangle with A C; Perp; 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, cop_perp2__col with B C; Perp; CopR. } { apply col_permutation_5, cop_perp2__col with A B; Perp; CopR. } } { assert (HPer : Per A B C). { apply midpoint_thales with O'; Col. unfold is_circumcenter in *; spliter; Cong. } 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; Col. unfold is_circumcenter in *; spliter; Cong. } assert (HPar : Par_strict A C B C). { apply par_not_col_strict with B; Col. apply l12_9 with A B; [Cop..|apply perp_left_comm|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). { unfold is_circumcenter in *; spliter. apply cong_mid_perp_bisect; Cong. intro; treat_equalities; apply HABC; Col. } assert (HPer2 : Perp_bisect O' C' A B). { unfold is_circumcenter in *; spliter. apply cong_mid_perp_bisect; Cong. } apply l6_21 with O' A' C' O; Col. { assert (HRect : Rectangle B A' O' C'). { apply Per_mid_rectangle with A C; Perp; 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, cop_perp2__col with B C; Perp; CopR. } { apply col_permutation_5, cop_perp2__col with A B; Perp; CopR. } } { 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). { unfold is_circumcenter in *; spliter. apply l8_2, midpoint_thales with O; Col; Cong. } 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 circumcenter_cong in HIC1; spliter. apply cong_mid_perp_bisect; Cong. } assert (HPer2 : Perp_bisect O C' A B). { unfold is_circumcenter in *; spliter. apply cong_mid_perp_bisect; Cong. } apply l6_21 with O B' C' O'; Col. { assert (HRect : Rectangle A B' O C'). { apply Per_mid_rectangle with B C; Perp; 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, cop_perp2__col with A C; Perp; CopR. } { apply col_permutation_5, cop_perp2__col with A B; Perp; CopR. } } { assert (HPer : Per C A B). { unfold is_circumcenter in *; spliter. apply l8_2, midpoint_thales with O'; Col; Cong. } assert (H : Perp_bisect O O' B C /\ Perp_bisect O B' A C /\ Perp_bisect O C' A B). { apply circumcenter_perp_all; auto. } destruct H as [Hc [HPer3 HPer4]]; clear Hc. assert (HPer1 : Perp_bisect O' B' A C). { apply circumcenter_cong in HIC2; spliter; apply cong_mid_perp_bisect; Cong. } assert (HPer2 : Perp_bisect O' C' A B). { unfold is_circumcenter in *; spliter; apply cong_mid_perp_bisect; Cong. } apply l6_21 with O' B' C' O; Col. { assert (HRect : Rectangle A B' O' C'). { apply Per_mid_rectangle with B C; Perp; 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, cop_perp2__col with A C; Perp; CopR. } { apply col_permutation_5, cop_perp2__col with A B; Perp; CopR. } } { assert (H : Perp_bisect O A' B C /\ Perp_bisect O B' A C /\ Perp_bisect O C' A B). { apply circumcenter_perp_all; auto. } 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; auto. } 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'; try CopR. apply perp_col0 with O B'; Col; Perp. Perp. } assert (HFalse := not_par_strict_id C A B); apply HFalse; Par. } { apply col_permutation_2, cop_perp2__col with B C; Perp; CopR. } { apply col_permutation_5, cop_perp2__col with A C; Perp; CopR. } } } } } Qed.
imports: GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.exercises