proposition: Lemma prop_11_12 : forall A B C D X, TangentCC A B C D -> OnCircle X A B -> OnCircle X C D -> Col X A C.
proof: Proof. exact TangentCC_Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.tangency GeoCoq.Tarski_dev.Annexes.inscribed_angle