proposition: Lemma mid_onc2__perp : forall O P A B X, O <> X -> A <> B -> OnCircle A O P -> OnCircle B O P -> Midpoint X A B -> Perp O X A B.
proof: Proof. intros. assert(Per O X A). apply (mid_onc2__per O P A B X); auto. unfold Midpoint in *. spliter. apply per_perp_in in H4; auto. apply perp_in_perp in H4. apply perp_sym. apply (perp_col _ X); Perp. Col. intro. subst X. treat_equalities; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel