proposition: Lemma col_onc2_perp__mid : forall O P A B X, O<>X -> A<>B -> Col A B X -> OnCircle A O P -> OnCircle B O P -> Perp O X A B -> Midpoint X A B.
proof: Proof. intros O P A B X HOX HAB HCol HAOn HBOn HPerp. destruct (midpoint_existence A B) as [M HM]. cut (X = M). intro; subst; trivial. assert (HNCol : ~ Col A B O) by (destruct (perp_not_col2 A B O X); Perp; Col). apply (l8_18_uniqueness A B O); Col; Perp. apply perp_sym, mid_onc2__perp with P; auto. intro; subst; apply HNCol; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel