proposition: Lemma is_orthocenter_cases : forall A B C G, is_orthocenter G A B C \/ is_orthocenter G A C B \/ is_orthocenter G B A C \/ is_orthocenter G B C A \/ is_orthocenter G C A B \/ is_orthocenter G C B A -> is_orthocenter G A B C.
proof: Proof. intros. decompose [or] H;clear H; unfold is_orthocenter in *;spliter; repeat (split; finish). Qed.
imports: GeoCoq.Highschool.circumcenter