proposition: Lemma prop_3_2 : 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. exact col_onc2_perp__mid. Qed.
imports: GeoCoq.Tarski_dev.Annexes.tangency GeoCoq.Tarski_dev.Annexes.inscribed_angle