proposition: Lemma inter_tangent_circle : forall P Q O M, P <> Q -> Cong P O Q O -> Col P O Q -> Le P M P O -> Le Q M Q O -> M = O.
proof: Proof. intros. assert(P = Q \/ Midpoint O P Q). apply(l7_20 O P Q H1);Cong. induction H4. contradiction. unfold Midpoint in *. spliter. assert(Le Q M P O). { apply (l5_6 Q M Q O Q M P O H3); Cong. } assert(Le P M O P). { apply(l5_6 P M P O P M O P); Cong. } assert(Le Q M O Q). { apply(l5_6 Q M Q O Q M O Q); Cong. } unfold Le in H7. unfold Le in H8. ex_and H7 A. ex_and H8 B. assert(Bet A O B); eBetween. assert(Le P Q A B). { apply(triangle_inequality_2 P M Q A O B); Cong. } assert(Le A B P Q). { apply(bet2_le2__le O O P Q A B); Between. unfold Le. exists A; Cong. exists B; Cong. } assert(Cong A B P Q). { apply le_anti_symmetry; auto. } assert(B = Q /\ P = A). apply(bet_cong_eq P A B Q);eBetween. spliter. subst A. subst B. clean_trivial_hyps. apply eq_sym. apply (l4_18 P Q O M); Cong; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order