proposition: Lemma tangency_chara : forall A B O P, P <> O -> (exists X, OnCircle X O P /\ Perp_at X A B O X) <-> Tangent A B O P.
proof: Proof. intros. split. intro. ex_and H0 T. unfold Tangent. unfold unique. exists T. split. split; auto. apply perp_in_col in H1. tauto. intros. spliter. assert(Col A B T). apply perp_in_col in H1. tauto. induction(eq_dec_points T x'). auto. apply False_ind. assert(Perp T x' O T). apply (perp_col2 A B); auto. apply perp_in_perp in H1. auto. assert(Perp_at T T x' O T). apply perp_perp_in; auto. assert(Per x' T O). apply perp_in_comm in H7. apply perp_in_per; auto. assert(~Col x' T O). apply perp_not_col in H6. ColR. assert(Lt T x' x' O /\ Lt T O x' O). assert_diffs. apply(l11_46 x' T O); auto. unfold OnCircle in *. unfold Lt in H10. spliter. apply H12. apply cong_transitivity with O P; Cong. intros. assert(HT:=H0). unfold Tangent in H0. unfold unique in H0. ex_and H0 T. assert(TangentAt A B O P T). unfold TangentAt. repeat split; auto. exists T. split; auto. assert(HH:=tangentat_perp A B O P T). assert(Perp A B O T). apply HH; auto. apply(l8_14_2_1b_bis A B O T T H4); Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms