proposition: Lemma prop_4 : forall O P A B C D X, B <> C -> A <> B -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OnCircle D O P -> Midpoint X A C -> Midpoint X B D -> X = O.
proof: Proof. exact mid2_onc4__eq. Qed.
imports: GeoCoq.Tarski_dev.Annexes.tangency GeoCoq.Tarski_dev.Annexes.inscribed_angle