proposition: Lemma orthocenter_per : forall A B C H, Per A B C -> is_orthocenter H A B C -> H=B.
proof: Proof. intros. unfold is_orthocenter in *;spliter. assert_diffs. assert (Perp A B B C) by (apply per_perp;finish). assert (Par A H A B) by (apply l12_9 with B C;Cop). assert (Col A B H) by (perm_apply (par_id A B H)). assert (Par C H B C) by (apply l12_9 with A B;finish). assert (Col B C H) by (perm_apply (par_id C B H)). apply l6_21 with A B C B;finish. Qed.
imports: GeoCoq.Highschool.circumcenter