proposition: Lemma tangency_chara3 : forall A B O P Q, A <> B -> OnCircle Q O P -> Col Q A B -> ((forall X, Col A B X -> OutCircle X O P) <-> Tangent A B O P).
proof: Proof. intros. split. intros. assert(HT:= (tangency_chara2 A B O P Q H0 H1)); auto. apply HT. intros. induction(eq_dec_points X Q). left; auto. right. assert(OutCircle X O P). apply H2; Col. unfold OutCircleS. unfold OutCircle in H5. unfold Lt. split; auto. intro. assert(HH:=midpoint_existence X Q). ex_and HH M. assert(InCircleS M O P). apply(bet_inc2__incs O P Q X M); Circle. intro. subst M. apply l7_2 in H7. apply is_midpoint_id in H7. subst X; tauto. intro. subst M. apply is_midpoint_id in H7. contradiction. unfold Midpoint in H7. spliter. Between. assert(Col A B M). unfold Midpoint in *. spliter. ColR. assert(HH:=(H2 M H9)). unfold InCircleS in *. unfold OutCircle in *. apply le__nlt in HH. contradiction. intros. assert(TangentAt A B O P Q). unfold TangentAt. repeat split; Col. induction(eq_dec_points X Q). subst X. unfold TangentAt in *. spliter. apply onc__outc; auto. assert(OutCircleS X O P). apply(tangent_out A B O P Q X); auto. unfold OutCircleS in *. unfold OutCircle. unfold Lt in H6. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms