proposition: Lemma orthocenter_col : forall A B C H, Col H B C -> is_orthocenter H A B C -> H = B \/ H = C.
proof: Proof. intros. unfold is_orthocenter in *. spliter. assert (Perp_at H B C A H). apply l8_14_2_1b_bis;finish. induction (eq_dec_points B H). subst;auto. assert (Perp A H B H) by (apply (perp_col1 A H B C H);finish). assert (Par A H A C) by (apply l12_9 with B H;finish). assert (Col H A C) by (perm_apply (par_id A C H)). assert (H=C). assert_diffs. apply l6_21 with B C A C;finish. subst. auto. Qed.
imports: GeoCoq.Highschool.circumcenter