proposition: Lemma tangent_construction : forall O P X, segment_circle -> OutCircle X O P -> exists Y, Tangent X Y O P.
proof: Proof. intros. induction(eq_dec_points O P). subst P. exists O. unfold Tangent. unfold unique. unfold OnCircle in *. exists O. repeat split; Col; Cong. intros. spliter. treat_equalities; auto. assert(O <> X). { intro. rewrite H2 in *;clear H2. treat_equalities. intuition. } assert(HH:=circle_cases O P X). induction HH. assert(HH:= perp_exists X O X H2). ex_and HH Y. unfold OnCircle in *. exists Y. apply tangency_chara; auto. exists X. apply perp_perp_in in H4. split; Circle. induction H3. unfold OutCircle in *. unfold InCircleS in *. apply lt__nle in H3; contradiction. assert(exists Q : Tpoint, OnCircle Q O P /\ Out O X Q). { apply(onc_exists); auto. } ex_and H4 U. assert(Bet O U X). { unfold Out in H5. spliter. induction H7. unfold OutCircleS in *. unfold OnCircle in *. assert(Le O X O U). { unfold Le. exists X. split; Cong. } assert(Lt O U O X). { apply(cong2_lt__lt O P O X); Cong. } apply le__nlt in H8. contradiction. assumption. } assert(exists X : Tpoint, Perp U X O U). { apply(perp_exists U O U). intro. unfold OnCircle in H4. treat_equalities; tauto. } ex_and H7 R. assert(HP:=symmetric_point_construction X O). ex_and HP W. unfold Midpoint in *. spliter. assert(exists X0 : Tpoint, (Bet U R X0 \/ Bet U X0 R) /\ Cong U X0 W X). { apply(segment_construction_2 R U W X). apply perp_distinct in H8. spliter. auto. } ex_and H10 T. assert(InCircleS U O X). { unfold InCircleS. unfold OutCircleS in H3. unfold OnCircle in H4. apply(cong2_lt__lt O P O X); Cong. } assert(OutCircleS T O X). { apply(diam_cong_incs__outcs O X X W U T); auto. unfold Diam. unfold OnCircle. repeat split; Cong. Cong. } unfold segment_circle in H. assert(exists Z : Tpoint, Bet U Z T /\ OnCircle Z O X). { apply(H O X U T). apply incs__inc; auto. apply outcs__outc; auto. } ex_and H14 Y. assert(exists Q : Tpoint, OnCircle Q O P /\ Out O Y Q). { apply(onc_exists O P Y); auto. intro. unfold OnCircle in H15. treat_equalities; tauto. } ex_and H16 V. exists V. assert(Bet O V Y). { unfold Out in H17. spliter. induction H19. unfold OutCircleS in H3. assert(Lt O V O Y). { apply (cong2_lt__lt O P O X); Cong. } unfold OnCircle in *. assert(Le O Y O V). { unfold Le. exists Y. split; Cong. } apply le__nlt in H21. contradiction. assumption. } assert(Cong O X O Y) by Cong. assert(Cong O U O V) by (apply cong_transitivity with O P; Cong). assert(CongA X O V Y O U). { unfold OnCircle in *. apply(l11_10 U O Y Y O U X V Y U). apply conga_left_comm. apply conga_refl; intro;treat_equalities; tauto. repeat split; try(intro;treat_equalities; tauto). right; auto. repeat split; try(intro;treat_equalities; tauto). left; auto. apply out_trivial; intro;treat_equalities; tauto. apply out_trivial; intro;treat_equalities; tauto. } assert(Cong V X U Y). { apply(cong2_conga_cong V O X U O Y); Cong. CongA. } assert(CongA O U Y O V X). { unfold OnCircle in *. apply(cong3_conga O U Y O V X). intro;treat_equalities; tauto. intro;treat_equalities. unfold OutCircleS in *. unfold Lt in *. spliter. Cong. repeat split; Cong. } assert(Per O V X). { apply(l11_17 O U Y O V X). apply(perp_col _ _ _ _ Y) in H8. apply perp_perp_in in H8. apply perp_in_comm in H8. apply perp_in_per. apply perp_in_sym. apply perp_in_comm. assumption. intro. treat_equalities. unfold CongA in H23. tauto. induction H10; ColR. assumption. } apply tangency_chara; auto. exists V. split; auto. apply per_perp_in in H24; Cong. apply perp_in_left_comm. apply perp_in_sym. assumption. unfold OnCircle in *. intro. treat_equalities; tauto. intro. treat_equalities. unfold CongA in H23. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms