proposition: Lemma prop_9 : forall O P X A B C, A <> B -> A <> C -> B <> C -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Cong X A X B -> Cong X A X C -> X = O.
proof: Proof. exact cong2_onc3__eq. Qed.
imports: GeoCoq.Tarski_dev.Annexes.tangency GeoCoq.Tarski_dev.Annexes.inscribed_angle