proposition: Lemma tangentat_perp : forall A B O P T, O <> P -> TangentAt A B O P T -> Perp A B O T.
proof: Proof. intros. assert(TA:=H0). unfold TangentAt in H0. spliter. assert(A <> B). apply (tangent_neq A B O P); auto. assert(~Col A B O). intro. assert(~Tangent A B O P). apply(diam_not_tangent); Col. contradiction. assert(HH:= l8_18_existence A B O H4). ex_and HH R. induction(eq_dec_points T R). subst R. auto. assert(HH:= (symmetric_point_construction T R)). ex_and HH T'. induction(eq_dec_points A R). subst A. assert(Perp T R R O). apply perp_comm. apply (perp_col R B O R T); Col. assert(Perp_at R T R R O). apply perp_in_comm. apply perp_perp_in. Perp. assert(Per O R T). apply l8_2. apply perp_in_per; auto. unfold Per in *. ex_and H11 T''. assert(T' = T''). apply (symmetric_point_uniqueness T R T' T''); auto. subst T''. assert(T <> T'). intro. subst T'. apply H7. apply sym_equal. apply l7_3; auto. assert(OnCircle T' O P). unfold OnCircle in *. apply cong_transitivity with O T; Cong. assert(OutCircleS T' O P). apply (tangent_out R B O P T T'); ColR. unfold OutCircleS in *. unfold Lt in *. spliter. unfold OnCircle in H14. apply False_ind. apply H16. Cong. assert(Perp T R R O). apply perp_comm. apply (perp_col R A O R T); Col. apply perp_left_comm. eapply (perp_col A B O R R); auto. unfold Midpoint in *. spliter. apply bet_col in H8. ColR. assert(Perp_at R T R R O). apply perp_in_comm. apply perp_perp_in. Perp. assert(Per O R T). apply l8_2. apply perp_in_per; auto. unfold Per in *. ex_and H12 T''. assert(T' = T''). apply (symmetric_point_uniqueness T R T' T''); auto. subst T''. assert(T <> T'). intro. subst T'. apply H7. apply sym_equal. apply l7_3; auto. assert(OnCircle T' O P). unfold OnCircle in *. apply cong_transitivity with O T; Cong. assert(OutCircleS T' O P). unfold Midpoint in *. spliter. apply bet_col in H12. apply (tangent_out A B O P T T'); auto. ColR. unfold OutCircleS in *. unfold Lt in *. spliter. unfold OnCircle in H14. apply False_ind. apply H17. Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms