proposition: Lemma diam_not_tangent : forall O P A B, P <> O -> Col O A B -> ~ Tangent A B O P.
proof: Proof. intros O P A B HOP HCol HTan. destruct HTan as [Q [[HQCol HQOn] HQUnique]]. destruct(eq_dec_points A B). subst B. destruct (segment_construction Q O O P) as [Q' [HQ'1 HQ'2]]. assert (HQQ' : Q <> Q') by (intro; treat_equalities; auto). apply HQQ', HQUnique; split; Col. destruct (diff_col_ex3 A B O) as [C [HOC [HAC [HBC HColC]]]]; Col. destruct (diam_points O P C) as [Q1 [Q2 [HBet [HQ1Q2C [HQ1On HQ2On]]]]]. assert (HQ1Q2 : Q1 <> Q2). intro; treat_equalities; auto. assert(Q = Q1) by (apply HQUnique; split; ColR). assert(Q = Q2) by (apply HQUnique; split; ColR). treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms