proposition: Lemma tangent_neq : forall A B O P, O<>P -> Tangent A B O P -> A<>B.
proof: Proof. intros. intro. subst B. unfold Tangent in *. unfold unique in *. ex_and H0 T. assert(HH:=symmetric_point_construction T O). ex_and HH T'. assert(OnCircle T' O P). apply (symmetric_oncircle T T' O P); auto. assert(T = T'). apply H1. split; Col. subst T'. apply H. apply l7_3 in H3. subst T. unfold OnCircle in H2. treat_equalities; tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Axioms.continuity_axioms