proposition: Lemma altitude_intersect: forall A A1 B B1 C C1 O: Tpoint, ~ Col A B C -> Perp A A1 B C -> Perp B B1 A C -> Perp C C1 A B -> Col O A A1 -> Col O B B1 -> Col O C C1.
proof: Proof. Proof with finish. intros A A1 B B1 C C1 O HNC HPerp1 HPerp2 HPerp3 HC1 HC2. assert (HT := HNC). apply construct_triangle in HT. destruct HT as [D [E [F HT]]]. spliter. assert (Midpoint A E F) by (apply diff_not_col_col_par4_mid with B C; finish). assert (Midpoint B D F) by (apply diff_not_col_col_par4_mid with A C; finish). assert (Midpoint C D E) by (apply diff_not_col_col_par4_mid with A B; finish). assert_diffs. elim (eq_dec_points A O); intro. treat_equalities; apply col_permutation_4; apply cop_perp2__col with A B... apply perp_right_comm; apply perp_col1 with B1... elim (eq_dec_points B O); intro. treat_equalities; apply col_permutation_4; apply cop_perp2__col with A B... apply perp_col1 with A1... elim (eq_dec_points C O); intro. subst; Col. assert (Perp_bisect A O E F) by (apply altitude_is_perp_bisect with B C A1; finish). assert (Perp_bisect B O D F) by (apply altitude_is_perp_bisect with A C B1; finish). assert (Perp O C D E). apply circumcenter_intersect with F A B; finish. apply perp_bisect_sym_1; assumption. apply perp_bisect_sym_1; assumption. assert (Perp C1 C D E). apply perp_sym; apply cop_par_perp__perp with A B... apply par_symmetry; apply par_col_par_2 with C... apply col_permutation_2; apply cop_perp2__col with D E; Perp. apply coplanar_pseudo_trans with A B C; Cop. apply coplanar_perm_2, col_cop__cop with B1; Col; Cop. Qed.
imports: GeoCoq.Highschool.circumcenter