proposition: Lemma is_orthocenter_coplanar : forall A B C H, is_orthocenter H A B C -> Coplanar H A B C.
proof: Proof. intros A B C H [HNCol [HPerp]]. apply coplanar_perm_6, perp__coplanar, HPerp. Qed.
imports: GeoCoq.Highschool.circumcenter