proposition: Lemma cop_mid_onc2_perp__col : forall O P A B X Y, A <> B -> OnCircle A O P -> OnCircle B O P -> Midpoint X A B -> Perp X Y A B -> Coplanar O A B Y -> Col X Y O.
proof: Proof. intros O P A B X Y HAB HAOn HBOn HX HPerp HCop. destruct (eq_dec_points O X). subst; Col. apply cop_perp2__col with A B; Cop. apply perp_left_comm, mid_onc2__perp with P; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel