proposition: Lemma 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 -> Col X Y O.
proof: Proof. intros O P A B X Y HAB HAOn HBOn HX HPerp. assert (HCop := all_coplanar O A B Y). apply cop_mid_onc2_perp__col with P A B; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel