proposition: Lemma concyclic_not_col_or_eq_aux : forall A B C D, Concyclic A B C D -> A = B \/ A = C \/ B = C \/ ~ Col A B C.
proof: Proof. intros A B C D HC. elim (eq_dec_points A B); intro HAB; Col. elim (eq_dec_points A C); intro HAC; Col. elim (eq_dec_points B C); intro HBC; Col5. right; right; right; intro HCol. destruct HC as [HCop [O [HCong1 [HCong2 HCong3]]]]. assert (H := midpoint_existence A B); destruct H as [M1 HMid1]. assert (HOM1 : O <> M1). { intro; treat_equalities. assert (H := l7_20 O A C); elim H; clear H; try intro H; Cong; try (apply HBC; apply symmetric_point_uniqueness with A O; Col); assert_cols; ColR. } assert (H := midpoint_existence A C); destruct H as [M2 HMid2]. assert (HOM2 : O <> M2). { intro; treat_equalities. assert (H := l7_20 O A B); elim H; clear H; try intro H; Cong; try (apply HBC; apply symmetric_point_uniqueness with A O; Col); assert_cols; ColR. } assert (HM1M2 : M1 <> M2) by (intro; treat_equalities; Col). assert (HPerp1 : Perp_bisect O M1 A B) by (apply cong_mid_perp_bisect; spliter; Cong). assert (HPerp2 : Perp_bisect O M2 A C) by (apply cong_mid_perp_bisect; spliter; Cong). assert (HOM1M2 : ~ Col O M1 M2). { intro HOM1M2; assert (H := l7_20 O A B); elim H; clear H; try intro H; Cong; try (apply HOM1; apply l7_17 with A B; Col); assert_diffs; assert_cols; ColR. } assert (HPar_strict : Par_strict O M1 O M2). { apply par_not_col_strict with M2; Col. apply l12_9 with A B; try CopR. apply coplanar_perm_16, col_cop__cop with C; Col; Cop. apply perp_bisect_perp; Col. apply perp_col0 with A C; Col; perm_apply perp_bisect_perp. } assert (H := not_par_strict_id O M1 M2); Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.circumcenter GeoCoq.Highschool.orthocenter GeoCoq.Highschool.midpoint_thales GeoCoq.Highschool.concyclic GeoCoq.Highschool.gravityCenter