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