proposition: Lemma is_orthocenter_perm : forall A B C G, is_orthocenter G A B C -> 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.
proof: Proof. intros. unfold is_orthocenter in *. spliter. repeat split;finish. Qed.
imports: GeoCoq.Highschool.circumcenter