proposition: Lemma tangency_chara2 : forall A B O P Q, OnCircle Q O P -> Col Q A B -> ((forall X, Col A B X -> X = Q \/ OutCircleS X O P) <-> Tangent A B O P).
proof: Proof. intros. split. intros. unfold Tangent. unfold unique. exists Q. repeat split; Col. intros. spliter. assert(HH:=(H1 x' H2)). induction HH. auto. unfold OnCircle in *. unfold OutCircleS in *. unfold Lt in *. spliter. apply False_ind. apply H5; Cong. intros. assert(TangentAt A B O P Q). unfold TangentAt. repeat split; Col. induction(eq_dec_points X Q). left; auto; unfold Tangent in H1. right. apply(tangent_out A B O P Q X); auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms