proposition: Lemma concyclic_not_col_or_eq : forall A B C A', Concyclic A B C A' -> A'=C \/ A'=B \/ A=B \/ A=C \/ A=A' \/ (~ Col A B A' /\ ~ Col A C A').
proof: Proof. intros A B C A' H. assert (H' := H); apply concyclic_perm_1 in H; apply concyclic_perm_3 in H'. apply concyclic_not_col_or_eq_aux in H; apply concyclic_not_col_or_eq_aux in H'. elim (eq_dec_points A' C); intro; try tauto. elim (eq_dec_points A' B); intro; try tauto. elim (eq_dec_points A B); intro; try tauto. elim (eq_dec_points A C); intro; try tauto. elim (eq_dec_points A A'); intro; try tauto. do 3 (elim H; clear H; intro H; try tauto); Col. do 3 (elim H'; clear H'; intro H'; try tauto); 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