proposition: Lemma tangent_out : forall A B O P T X, X <> T -> Col A B X -> TangentAt A B O P T -> OutCircleS X O P.
proof: Proof. intros. unfold TangentAt in *. spliter. induction(eq_dec_points O P). subst P. unfold OutCircleS. unfold Lt. split. apply le_trivial. intro. unfold OnCircle in *. assert(T = O). apply cong_identity with O; Cong. assert(X = O). apply cong_identity with O; Cong. subst O. contradiction. assert(InCircle X O P -> X = T). intro. assert(HH:= chord_completion O P T X H3 H5). ex_and HH T'. assert(A <> B). apply (tangent_neq A B O P); auto. unfold Tangent in *. unfold unique in *. ex_and H1 TT. assert(TT= T). apply H9. split; auto. subst TT. assert(T = T'). apply H9. split; auto. apply bet_col in H7. assert(Col A X T); ColR. subst T'. apply between_identity in H7. subst X. tauto. assert(~InCircle X O P). intro. apply H5 in H6. contradiction. apply ninc__outcs. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms