Require Export GeoCoq.Tarski_dev.Annexes.circles.
Require Export GeoCoq.Axioms.continuity_axioms.

Section Tangency.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** Euclid Book III, Prop 11 and Prop 12
 We do not need to distinguish between internal or external tangency. *)

(** If two circles are tangent, the common point is on the line joining the centers. *)

Lemma TangentCC_Col : forall A B C D X,
 TangentCC A B C D ->
 OnCircle X A B ->
 OnCircle X C D ->
 Col X A C.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
unfold TangentCC in *.

(* Goal: @Col Tn X A C *)
induction(eq_dec_points A C).
(* Goal: False *)
subst C.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Col.

(* Goal: @Col Tn X A C *)
assert(HS:=ex_sym1 A C X H2).
(* Goal: @Col Tn X A C *)
ex_and HS Y.
(* Goal: @Col Tn X A C *)
ex_and H4 M.

(* Goal: @Col Tn X A C *)
assert(Cong X A Y A).
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply(is_image_col_cong A C X Y A H2 H6); Col.
(* Goal: @Col Tn X A C *)
assert(Cong X C Y C).
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply(is_image_col_cong A C X Y C H2 H6); Col.

(* Goal: @Col Tn X A C *)
destruct H.
(* Goal: @Col Tn X A C *)
unfold unique in H.

(* Goal: @Col Tn X A C *)
assert(x =X).
(* Goal: False *)
apply H.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
split; auto.
(* Goal: @Col Tn X A C *)
subst x.
(* Goal: @Col Tn X A C *)
assert(OnCircle Y A B).
(* Goal: False *)
unfold OnCircle in *.
(* Goal: @Cong Tn A Y A B *)
(* Goal: @Col Tn X A C *)
apply cong_transitivity with A X; Cong.
(* Goal: @Col Tn X A C *)
assert(OnCircle Y C D).
(* Goal: False *)
unfold OnCircle in *.
(* Goal: @Cong Tn C Y C D *)
(* Goal: @Col Tn X A C *)
apply cong_transitivity with C X; Cong.
(* Goal: @Col Tn X A C *)
assert(X = Y).
(* Goal: False *)
apply H.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
split; auto.
(* Goal: @Col Tn X A C *)
subst Y.

(* Goal: @Col Tn X A C *)
unfold Reflect in H6.
(* Goal: @Col Tn X A C *)
induction H6.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @Col Tn X A C *)
(* Goal: @Col Tn X A C *)
unfold ReflectL in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @Col Tn X A C *)
(* Goal: @Col Tn X A C *)
ex_and H11 Z.

(* Goal: @Col Tn X A C *)
(* Goal: @Col Tn X A C *)
assert(Z = X).
(* Goal: @eq (@Tpoint Tn) R T *)
(* Goal: @Perp Tn A B O T *)
apply l7_3; auto.
(* Goal: @Col Tn X A C *)
(* Goal: @Col Tn X A C *)
subst Z.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Col.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
contradiction.
Qed.

Lemma tangent_neq : forall A B O P,
 O<>P -> Tangent A B O P -> A<>B.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
(* Goal: False *)
subst B.
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
unfold Tangent in *.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
unfold unique in *.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
ex_and H0 T.
(* Goal: False *)
assert(HH:=symmetric_point_construction T O).
(* Goal: @Perp Tn A B O T *)
ex_and HH T'.
(* Goal: @Perp Tn A B O T *)
assert(OnCircle T' O P).
(* Goal: @OnCircle Tn T' O P *)
(* Goal: False *)
apply (symmetric_oncircle T T' O P); auto.
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
assert(T = T').
(* Goal: @eq (@Tpoint Tn) T T' *)
(* Goal: False *)
apply H1.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
split; Col.
(* Goal: False *)
(* Goal: @Perp Tn A B O T *)
subst T'.
(* Goal: False *)
apply H.
(* Goal: @eq (@Tpoint Tn) O P *)
apply l7_3 in H3.
(* Goal: False *)
subst T.
(* Goal: @eq (@Tpoint Tn) O P *)
unfold OnCircle in H2.
(* Goal: False *)
treat_equalities; tauto.
Qed.

(** A line going through the center is not tangent to the circle. *)

Lemma diam_not_tangent : forall O P A B, 
  P <> O -> Col O A B -> ~ Tangent A B O P.
Proof.
(* Goal: forall (O P A B : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P O)) (_ : @Col Tn O A B), not (@Tangent Tn A B O P) *)
intros O P A B HOP HCol HTan.
(* Goal: False *)
destruct HTan as [Q [[HQCol HQOn] HQUnique]].
(* Goal: False *)
destruct(eq_dec_points A B).
(* Goal: False *)
(* Goal: False *)
  subst B.
(* Goal: False *)
(* Goal: False *)
  destruct (segment_construction Q O O P) as [Q' [HQ'1 HQ'2]].
(* Goal: False *)
(* Goal: False *)
  assert (HQQ' : Q <> Q') by (intro; treat_equalities; auto).
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
  apply HQQ', HQUnique; split; Col.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
destruct (diff_col_ex3 A B O) as [C [HOC [HAC [HBC HColC]]]]; Col.
(* Goal: False *)
destruct (diam_points O P C) as [Q1 [Q2 [HBet [HQ1Q2C [HQ1On HQ2On]]]]].
(* Goal: False *)
assert (HQ1Q2 : Q1 <> Q2).
(* Goal: not (@eq (@Tpoint Tn) Q1 Q2) *)
(* Goal: False *)
  intro; treat_equalities; auto.
(* Goal: False *)
assert(Q = Q1) by (apply HQUnique; split; ColR).
(* Goal: False *)
assert(Q = Q2) by (apply HQUnique; split; ColR).
(* Goal: False *)
treat_equalities; auto.
Qed.

(** Every point on the tangent different from the point of tangency is strictly outside the circle. *)

Lemma tangent_out : forall A B O P T X,
  X <> T -> Col A B X -> TangentAt A B O P T -> OutCircleS X O P.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @OutCircle Tn Q O P *)
(* Goal: @OutCircle Tn X O P *)
unfold TangentAt in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.

(* Goal: @OutCircleS Tn X O P *)
induction(eq_dec_points O P).
(* Goal: @OutCircleS Tn X O P *)
(* Goal: @OutCircleS Tn X O P *)
subst P.
(* Goal: @OutCircleS Tn X O P *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold OutCircleS.
(* Goal: @Lt Tn O P O X *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold Lt.

(* Goal: iff (@Cong Tn A X A B) (@Cong Tn A X A D) *)
split.
(* Goal: @Le Tn O O O X *)
(* Goal: not (@Cong Tn O O O X) *)
(* Goal: @OutCircleS Tn X O P *)
apply le_trivial.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
unfold OnCircle in *.
(* Goal: False *)
(* Goal: @OutCircleS Tn X O P *)
assert(T = O).
(* Goal: @eq (@Tpoint Tn) X O *)
(* Goal: False *)
(* Goal: @OutCircleS Tn X O P *)
apply cong_identity with O; Cong.
(* Goal: False *)
(* Goal: @OutCircleS Tn X O P *)
assert(X = O).
(* Goal: @eq (@Tpoint Tn) X O *)
(* Goal: False *)
(* Goal: @OutCircleS Tn X O P *)
apply cong_identity with O; Cong.
(* Goal: False *)
(* Goal: @OutCircleS Tn X O P *)
subst O.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
contradiction.

(* Goal: @OutCircleS Tn X O P *)
assert(InCircle X O P -> X = T).
(* Goal: not (@Col Tn A C P) *)
intro.

(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
assert(HH:= chord_completion O P T X H3 H5).
(* Goal: @Perp Tn A B O T *)
ex_and HH T'.
(* Goal: @Perp Tn A B O T *)
assert(A <> B).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Perp Tn A B O T *)
apply (tangent_neq A B O P); auto.
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
unfold Tangent in *.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
unfold unique in *.
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
ex_and H1 TT.
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
assert(TT= T).
(* Goal: @eq (@Tpoint Tn) T T' *)
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
apply H9.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
split; auto.
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
subst TT.
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
assert(T = T').
(* Goal: @eq (@Tpoint Tn) T T' *)
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
apply H9.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
split; auto.
(* Goal: @Col Tn A B T' *)
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
apply bet_col in H7.

(* Goal: @Col Tn A B T' *)
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
assert(Col A X T); ColR.
(* Goal: False *)
(* Goal: @Perp Tn A B O T *)
subst T'.
(* Goal: @eq (@Tpoint Tn) X T *)
(* Goal: @OutCircleS Tn X O P *)
apply between_identity in H7.
(* Goal: @OutCircle Tn X O P *)
(* Goal: @OutCircle Tn X O P *)
subst X.
(* Goal: @Le Tn O P O X *)
tauto.

(* Goal: @OutCircleS Tn X O P *)
assert(~InCircle X O P).
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
(* Goal: @OutCircleS Tn X O P *)
apply H5 in H6.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
contradiction.
(* Goal: @OutCircleS Tn X O P *)
apply ninc__outcs.
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assumption.
Qed.

(** If line AB is tangent to a circle of center O at a point T, then OT is perpendicular to AB.
This is Euclid Book III, Prop 18 *)

Lemma tangentat_perp : 
forall A B O P T, O <> P -> TangentAt A B O P T -> Perp A B O T.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @Perp Tn A B O T *)
assert(TA:=H0).
(* Goal: @Perp Tn A B O T *)
unfold TangentAt in H0.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @Perp Tn A B O T *)
assert(A <> B).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Perp Tn A B O T *)
apply (tangent_neq A B O P); auto.
(* Goal: @Perp Tn A B O T *)
assert(~Col A B O).
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
(* Goal: @Perp Tn A B O T *)
assert(~Tangent A B O P).
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply(diam_not_tangent); Col.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
contradiction.

(* Goal: @Perp Tn A B O T *)
assert(HH:= l8_18_existence A B O H4).
(* Goal: @Perp Tn A B O T *)
ex_and HH R.

(* Goal: @Perp Tn A B O T *)
induction(eq_dec_points T R).
(* Goal: @Perp Tn A B O T *)
(* Goal: @Perp Tn A B O T *)
subst R.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
auto.

(* Goal: @Perp Tn A B O T *)
assert(HH:= (symmetric_point_construction T R)).
(* Goal: @Perp Tn A B O T *)
ex_and HH T'.

(* Goal: @Perp Tn A B O T *)
induction(eq_dec_points A R).
(* Goal: @Perp Tn A B O T *)
(* Goal: @Perp Tn A B O T *)
subst A.
(* Goal: @Perp Tn A B O T *)
assert(Perp T R R O).
(* Goal: @Perp Tn T R R O *)
(* Goal: @Perp Tn A B O T *)
apply perp_comm.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply (perp_col R B O R T); Col.
(* Goal: @Perp Tn A B O T *)
assert(Perp_at R T R R O).
(* Goal: @Perp_at Tn R T R R O *)
(* Goal: @Perp Tn A B O T *)
apply perp_in_comm.
(* Goal: @Perp_at Tn R R T O R *)
(* Goal: @Perp Tn A B O T *)
apply perp_perp_in.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Perp.
(* Goal: @Perp Tn A B O T *)
assert(Per O R T).
(* Goal: @Per Tn O R T *)
(* Goal: @Perp Tn A B O T *)
apply l8_2.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply perp_in_per; auto.
(* Goal: @Perp Tn A B O T *)
unfold Per in *.
(* Goal: @Perp Tn R B O T *)
(* Goal: @Perp Tn A B O T *)
ex_and H11 T''.
(* Goal: @Perp Tn A B O T *)
assert(T' = T'').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply (symmetric_point_uniqueness T R T' T''); auto.
(* Goal: @Perp Tn A B O T *)
subst T''.

(* Goal: @Perp Tn A B O T *)
assert(T <> T').
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
(* Goal: @Perp Tn A B O T *)
subst T'.
(* Goal: False *)
(* Goal: @Perp Tn A B O T *)
apply H7.
(* Goal: @eq (@Tpoint Tn) T R *)
(* Goal: @Perp Tn A B O T *)
apply sym_equal.
(* Goal: @eq (@Tpoint Tn) R T *)
(* Goal: @Perp Tn A B O T *)
apply l7_3; auto.

(* Goal: @Perp Tn A B O T *)
assert(OnCircle T' O P).
(* Goal: False *)
unfold OnCircle in *.
(* Goal: @Cong Tn O T' O P *)
(* Goal: @Perp Tn A B O T *)
apply cong_transitivity with O T; Cong.

(* Goal: @Perp Tn A B O T *)
assert(OutCircleS T' O P).
(* Goal: @OutCircleS Tn T' O P *)
(* Goal: @Perp Tn R B O T *)
(* Goal: @Perp Tn A B O T *)
apply (tangent_out R B O P T T'); ColR.
(* Goal: @OutCircle Tn X O P *)
unfold OutCircleS in *.
(* Goal: @eq (@Tpoint Tn) Q x' *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold Lt in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @Perp Tn A B O T *)
unfold OnCircle in H14.
(* Goal: @eq (@Tpoint Tn) Z P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply False_ind.
(* Goal: False *)
(* Goal: @Perp Tn A B O T *)
apply H16.
(* Goal: @Cong Tn O P O T' *)
Cong.


(* Goal: @Perp Tn A B O T *)
assert(Perp T R R O).
(* Goal: @Perp Tn T R R O *)
(* Goal: @Perp Tn A B O T *)
apply perp_comm.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply (perp_col R A O R T); Col.
(* Goal: @Perp Tn R A O R *)
(* Goal: @Col Tn R A T *)
(* Goal: @Perp Tn A B O T *)
apply perp_left_comm.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
eapply (perp_col A B O R R); auto.
(* Goal: False *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @Col Tn R A T *)
(* Goal: @Perp Tn A B O T *)
apply bet_col in H8.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
eCol.
(* Goal: @Perp Tn A B O T *)
assert(Perp_at R T R R O).
(* Goal: @Perp_at Tn R T R R O *)
(* Goal: @Perp Tn A B O T *)
apply perp_in_comm.
(* Goal: @Perp_at Tn R R T O R *)
(* Goal: @Perp Tn A B O T *)
apply perp_perp_in.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Perp.


(* Goal: @Perp Tn A B O T *)
assert(Per O R T).
(* Goal: @Per Tn O R T *)
(* Goal: @Perp Tn A B O T *)
apply l8_2.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply perp_in_per; auto.
(* Goal: @Perp Tn A B O T *)
unfold Per in *.
(* Goal: @Perp Tn A B O T *)
ex_and H12 T''.
(* Goal: @Perp Tn A B O T *)
assert(T' = T'').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply (symmetric_point_uniqueness T R T' T''); auto.
(* Goal: @Perp Tn A B O T *)
subst T''.

(* Goal: @Perp Tn A B O T *)
assert(T <> T').
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
(* Goal: @Perp Tn A B O T *)
subst T'.
(* Goal: False *)
(* Goal: @Perp Tn A B O T *)
apply H7.
(* Goal: @eq (@Tpoint Tn) T R *)
(* Goal: @Perp Tn A B O T *)
apply sym_equal.
(* Goal: @eq (@Tpoint Tn) R T *)
(* Goal: @Perp Tn A B O T *)
apply l7_3; auto.

(* Goal: @Perp Tn A B O T *)
assert(OnCircle T' O P).
(* Goal: False *)
unfold OnCircle in *.
(* Goal: @Cong Tn O T' O P *)
(* Goal: @Perp Tn A B O T *)
apply cong_transitivity with O T; Cong.

(* Goal: @Perp Tn A B O T *)
assert(OutCircleS T' O P).
(* Goal: False *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @OutCircleS Tn T' O P *)
(* Goal: @Perp Tn A B O T *)
apply bet_col in H12.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply (tangent_out A B O P T T'); auto.
(* Goal: @Col Tn Q N Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
ColR.
(* Goal: @OutCircle Tn X O P *)
unfold OutCircleS in *.
(* Goal: @eq (@Tpoint Tn) Q x' *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold Lt in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @Perp Tn A B O T *)
unfold OnCircle in H14.
(* Goal: @eq (@Tpoint Tn) Z P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply False_ind.
(* Goal: False *)
apply H17.
(* Goal: @Cong Tn O P O T' *)
Cong.
Qed.

(** AB is tangent to the circle (O,P) iff they intersect at a point X
such that AB is perpendicular to OX. *)

Lemma tangency_chara : forall A B O P, P <> O ->
 (exists X, OnCircle X O P /\ Perp_at X A B O X) <-> Tangent A B O P.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.

(* Goal: iff (@Cong Tn A X A B) (@Cong Tn A X A D) *)
split.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
ex_and H0 T.
(* Goal: @Tangent Tn A B O P *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold Tangent.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn A B X) (@OnCircle Tn X O P))) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold unique.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
exists T.
(* Goal: iff (@Cong Tn A X A B) (@Cong Tn A X A D) *)
split.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
split; auto.
(* Goal: @Col Tn A B T *)
(* Goal: @eq (@Tpoint Tn) T x' *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
apply perp_in_col in H1.
(* Goal: @Le Tn O P O X *)
tauto.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @eq (@Tpoint Tn) T x' *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert(Col A B T).
(* Goal: @Col Tn A B T *)
(* Goal: @eq (@Tpoint Tn) T x' *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
apply perp_in_col in H1.
(* Goal: @Le Tn O P O X *)
tauto.

(* Goal: @eq (@Tpoint Tn) T x' *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
induction(eq_dec_points T x').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
auto.
(* Goal: @eq (@Tpoint Tn) Z P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply False_ind.

(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert(Perp T x' O T).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply (perp_col2 A B); auto.
(* Goal: @Perp Tn A B O T *)
(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
apply perp_in_perp in H1.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
auto.

(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert(Perp_at T T x' O T).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply perp_perp_in; auto.

(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert(Per x' T O).
(* Goal: @Per Tn x' T O *)
(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
apply perp_in_comm in H7.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply perp_in_per; auto.

(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert(~Col x' T O).
(* Goal: not (@Col Tn x' T O) *)
(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
apply perp_not_col in H6.
(* Goal: @Col Tn Q N Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
ColR.

(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert(Lt T x' x' O /\ Lt T O x' O).
(* Goal: and (@Lt Tn T x' x' O) (@Lt Tn T O x' O) *)
(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert_diffs.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply(l11_46 x' T O); auto.
(* Goal: False *)
unfold OnCircle in *.
(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
unfold Lt in H10.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: False *)
(* Goal: forall _ : @Tangent Tn A B O P, @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
apply H12.
(* Goal: @Cong Tn O P O T' *)
apply cong_transitivity with O P; Cong.

(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert(HT:=H0).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
unfold Tangent in H0.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
unfold unique in H0.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
ex_and H0 T.

(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
assert(TangentAt A B O P T).
(* Goal: @TangentAt Tn A B O P Q *)
(* Goal: @OutCircle Tn X O P *)
unfold TangentAt.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X O P) (@Perp_at Tn X A B O X)) *)
exists T.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
split; auto.
(* Goal: @Perp_at Tn T A B O T *)
assert(HH:=tangentat_perp A B O P T).
(* Goal: @Perp_at Tn T A B O T *)
assert(Perp A B O T).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply HH; auto.

(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply(l8_14_2_1b_bis A B O T T H4); Col.
Qed.


Lemma tangency_chara2 : forall A B O P Q,
 OnCircle Q O P -> Col Q A B -> 
 ((forall X, Col A B X -> X = Q \/ OutCircleS X O P) <-> Tangent A B O P).
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: iff (@Cong Tn A X A B) (@Cong Tn A X A D) *)
split.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @Tangent Tn A B O P *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold Tangent.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn A B X) (@OnCircle Tn X O P))) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold unique.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X Q P) (@Col Tn X Q Z)) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
exists Q.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
repeat split; Col.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @eq (@Tpoint Tn) Q x' *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
assert(HH:=(H1 x' H2)).
(* Goal: @eq (@Tpoint Tn) Z P *)
induction HH.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
auto.
(* Goal: False *)
unfold OnCircle in *.
(* Goal: @OutCircle Tn X O P *)
unfold OutCircleS in *.
(* Goal: @eq (@Tpoint Tn) Q x' *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold Lt in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @eq (@Tpoint Tn) Z P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply False_ind.
(* Goal: @Cong Tn O P O T' *)
apply H5; Cong.

(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @OutCircle Tn X O P *)
assert(TangentAt A B O P Q).
(* Goal: @TangentAt Tn A B O P Q *)
(* Goal: @OutCircle Tn X O P *)
unfold TangentAt.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
repeat split; Col.

(* Goal: @OutCircle Tn X O P *)
induction(eq_dec_points X Q).
left; auto;

unfold Tangent in H1.
(* Goal: or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
right.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply(tangent_out A B O P Q X); auto.
Qed.


Lemma tangency_chara3 : forall A B O P Q, A <> B ->
 OnCircle Q O P -> Col Q A B -> 
 ((forall X, Col A B X -> OutCircle X O P) <-> Tangent A B O P).
Proof.

(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: iff (@Cong Tn A X A B) (@Cong Tn A X A D) *)
split.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assert(HT:= (tangency_chara2 A B O P Q H0 H1)); auto.
(* Goal: @Tangent Tn A B O P *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
apply HT.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @OutCircle Tn X O P *)
induction(eq_dec_points X Q).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
left; auto.
(* Goal: or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
right.
(* Goal: @OutCircleS Tn X O P *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
assert(OutCircle X O P).
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply H2; Col.

(* Goal: @OutCircleS Tn X O P *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold OutCircleS.
(* Goal: @Lt Tn O P O X *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold OutCircle in H5.
(* Goal: @Lt Tn O P O X *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold Lt.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
split; auto.
(* Goal: not (@Col Tn A C P) *)
intro.

(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
assert(HH:=midpoint_existence X Q).
(* Goal: @eq (@Tpoint Tn) Z P *)
ex_and HH M.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
assert(InCircleS M O P).
(* Goal: @InCircleS Tn M O P *)
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
apply(bet_inc2__incs O P Q X M); Circle.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: @Perp Tn A C Q P *)
(* Goal: @Perp Tn A C Q P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
subst M.

(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
(* Goal: @Bet Tn Q M X *)
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
apply l7_2 in H7.
(* Goal: False *)
(* Goal: @Bet Tn Q M X *)
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
apply is_midpoint_id in H7.
(* Goal: @Le Tn O P O X *)
subst X; tauto.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: @Perp Tn A C Q P *)
(* Goal: @Perp Tn A C Q P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
subst M.
(* Goal: False *)
(* Goal: @Bet Tn Q M X *)
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
apply is_midpoint_id in H7.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
contradiction.
(* Goal: @Bet Tn Q M X *)
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold Midpoint in H7.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @Bet Tn Q M X *)
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
Between.

(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
assert(Col A B M).
(* Goal: False *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @Col Tn Q N Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
ColR.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
assert(HH:=(H2 M H9)).
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold InCircleS in *.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold OutCircle in *.

(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
apply le__nlt in HH.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
contradiction.

(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @OutCircle Tn X O P *)
assert(TangentAt A B O P Q).
(* Goal: @TangentAt Tn A B O P Q *)
(* Goal: @OutCircle Tn X O P *)
unfold TangentAt.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
repeat split; Col.

(* Goal: @OutCircle Tn X O P *)
induction(eq_dec_points X Q).
(* Goal: @OutCircle Tn X O P *)
(* Goal: @OutCircle Tn X O P *)
subst X.
(* Goal: @OutCircle Tn Q O P *)
(* Goal: @OutCircle Tn X O P *)
unfold TangentAt in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply onc__outc; auto.

(* Goal: @OutCircle Tn X O P *)
assert(OutCircleS X O P).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply(tangent_out A B O P Q X); auto.
(* Goal: @OutCircle Tn X O P *)
unfold OutCircleS in *.
(* Goal: @OutCircle Tn X O P *)
unfold OutCircle.
(* Goal: @Le Tn O P O X *)
unfold Lt in H6.
(* Goal: @Le Tn O P O X *)
tauto.
Qed.

(** Euclid Book III Prop 5 
 If two circles cut one another, then they do not have the same center. *)

Lemma intercc__neq :  forall A B C D,
 InterCC A B C D -> A<>C.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
unfold InterCC in *.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
ex_and H P.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
ex_and H0 Q.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
unfold InterCCAt in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: False *)
unfold OnCircle in *.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
subst C.
(* Goal: False *)
apply H.
(* Goal: @EqC Tn A B A D *)
unfold EqC.
(* Goal: False *)
unfold OnCircle in *.
(* Goal: forall X : @Tpoint Tn, iff (@Cong Tn A X A B) (@Cong Tn A X A D) *)
assert(Cong A B A D) by (apply cong_transitivity with A P; Cong).
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: iff (@Cong Tn A X A B) (@Cong Tn A X A D) *)
split.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: @Cong Tn O P O T' *)
apply cong_transitivity with A B; Cong.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: @Cong Tn O P O T' *)
apply cong_transitivity with A D; Cong.
Qed.

(** Euclid Book III Prop 6 
If two circles touch one another, then they do not have the same center.
*)

Lemma tangentcc__neq: forall A B C D,
 A<>B ->
 TangentCC A B C D ->
 A<>C.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
unfold TangentCC in *.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
unfold unique in *.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
ex_and H0 T.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
subst C.
(* Goal: False *)
unfold OnCircle in *.
(* Goal: False *)
assert(Cong A B A D) by (apply cong_transitivity with A T; Cong).
(* Goal: False *)
assert(T = B).
(* Goal: @Cong Tn O P O T' *)
apply(H1 B); Cong.
(* Goal: False *)
subst T.
(* Goal: False *)
assert(HH:=symmetric_point_construction B A).
(* Goal: False *)
ex_and HH B'.
(* Goal: False *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: False *)
assert(B = B').
(* Goal: @Cong Tn O P O T' *)
  apply(H1 B'); split; Cong.
(* Goal: @Cong Tn O P O T' *)
  apply cong_transitivity with A B; Cong.
(* Goal: False *)
subst B'.
(* Goal: False *)
treat_equalities; tauto.
Qed.

Lemma interccat__neq : forall A B C D P Q, InterCCAt A B C D P Q -> A <> C.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
apply intercc__neq  with B D.
(* Goal: @InterCC Tn A B C D *)
unfold InterCC.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
exists P; exists Q;auto.
Qed.

(** Prop 17 construction of the tangent to a circle at a given point *)

Lemma tangent_construction : forall O P X, segment_circle -> OutCircle X O P 
                                                  -> exists Y, Tangent X Y O P.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @OutCircleS Tn X O P *)
induction(eq_dec_points O P).
(* Goal: @OutCircleS Tn X O P *)
(* Goal: @OutCircleS Tn X O P *)
subst P.
exists O.
(* Goal: @Tangent Tn A B O P *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold Tangent.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn A B X) (@OnCircle Tn X O P))) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
unfold unique.
(* Goal: False *)
unfold OnCircle in *.
exists O.
(* Goal: @Cong Tn O P O T' *)
repeat split; Col; Cong.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: False *)
treat_equalities; auto.

assert(O <> X).
{
(* Goal: not (@Col Tn A C P) *)
  intro.
  rewrite H2 in *;clear H2.
  treat_equalities.
  intuition.
}

assert(HH:=circle_cases O P X).
(* Goal: @eq (@Tpoint Tn) Z P *)
induction HH.

assert(HH:= perp_exists X O X H2).
ex_and HH Y.
(* Goal: False *)
unfold OnCircle in *.
exists Y.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply tangency_chara; auto.
exists X.
apply perp_perp_in in H4.
split; Circle.

induction H3.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold OutCircle in *.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
unfold InCircleS in *.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
apply lt__nle in H3; contradiction.


assert(exists Q : Tpoint, OnCircle Q O P /\ Out O X Q).
{
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  apply(onc_exists); auto.
}

ex_and H4 U.

assert(Bet O U X).
{
  unfold Out in H5.
(* Goal: @eq (@Tpoint Tn) Z P *)
  spliter.
  induction H7.
(* Goal: @OutCircle Tn X O P *)
  unfold OutCircleS in *.
(* Goal: False *)
  unfold OnCircle in *.
  assert(Le O X O U).
  {
    unfold Le.
    exists X.
(* Goal: @Cong Tn O P O T' *)
    split; Cong.
  }
  assert(Lt O U O X).
  {
(* Goal: @Cong Tn O P O T' *)
    apply(cong2_lt__lt O P O X); Cong.
  }
  apply le__nlt in H8.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
  contradiction.
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  assumption.
}

assert(exists X : Tpoint, Perp U X O U).
{
  apply(perp_exists U O U).
(* Goal: not (@Col Tn A C P) *)
  intro.
  unfold OnCircle in H4.
(* Goal: False *)
  treat_equalities; tauto.
}
ex_and H7 R.
assert(HP:=symmetric_point_construction X O).
ex_and HP W.
(* Goal: False *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
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.
(* Goal: @eq (@Tpoint Tn) Z P *)
  spliter.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  auto.
}

ex_and H10 T.

assert(InCircleS U O X).
{
  unfold InCircleS.
  unfold OutCircleS in H3.
  unfold OnCircle in H4.
(* Goal: @Cong Tn O P O T' *)
  apply(cong2_lt__lt O P O X); Cong.
}

assert(OutCircleS T O X).
{
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  apply(diam_cong_incs__outcs O X X W U T); auto.
  unfold Diam.
  unfold OnCircle.
(* Goal: @Cong Tn O P O T' *)
  repeat split; Cong.
(* Goal: @Cong Tn O P O T' *)
  Cong.
}
unfold segment_circle in H.
assert(exists Z : Tpoint, Bet U Z T /\ OnCircle Z O X).
{
  apply(H O X U T).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  apply incs__inc; auto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  apply outcs__outc; auto.
}

ex_and H14 Y.
assert(exists Q : Tpoint, OnCircle Q O P /\ Out O Y Q).
{
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  apply(onc_exists O P Y); auto.
(* Goal: not (@Col Tn A C P) *)
  intro.
  unfold OnCircle in H15.
(* Goal: False *)
  treat_equalities; tauto.
}
ex_and H16 V.

exists V.

assert(Bet O V Y).
{
  unfold Out in H17.
(* Goal: @eq (@Tpoint Tn) Z P *)
  spliter.
  induction H19.
  unfold OutCircleS in H3.
  assert(Lt O V O Y).
  {
(* Goal: @Cong Tn O P O T' *)
    apply (cong2_lt__lt O P O X); Cong.
  }
(* Goal: False *)
  unfold OnCircle in *.
  assert(Le O Y O V).
  {
    unfold Le.
    exists Y.
(* Goal: @Cong Tn O P O T' *)
    split; Cong.
  }
  apply le__nlt in H21.
(* Goal: False *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
  contradiction.
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  assumption.
}

(* Goal: @Cong Tn O P O T' *)
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).
{
(* Goal: False *)
  unfold OnCircle in *.
  apply(out_conga U O Y Y O U X V Y U).
  apply conga_left_comm.
(* Goal: False *)
  apply conga_refl; intro;treat_equalities; tauto.
  unfold Out.
  repeat split; try(intro;treat_equalities; tauto).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  left; auto.
  unfold Out.
  repeat split; try(intro;treat_equalities; tauto).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  right; auto.
(* Goal: False *)
  apply out_trivial;  intro;treat_equalities; tauto.
(* Goal: False *)
  apply out_trivial;  intro;treat_equalities; tauto.
}

assert(Cong V X U Y).
{

(* Goal: @Cong Tn O P O T' *)
  apply(cong2_conga_cong V O X U O Y); Cong.
  CongA.
}

assert(CongA O U Y O V X).
{
(* Goal: False *)
  unfold OnCircle in *.
  apply(cong3_conga O U Y O V X).
(* Goal: False *)
  intro;treat_equalities; tauto.
  intro;treat_equalities.
(* Goal: @OutCircle Tn X O P *)
  unfold OutCircleS in *.
(* Goal: @eq (@Tpoint Tn) Q x' *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), or (@eq (@Tpoint Tn) X Q) (@OutCircleS Tn X O P) *)
  unfold Lt in *.
(* Goal: @eq (@Tpoint Tn) Z P *)
  spliter.
  (assert (Cong O P O V) by finish;intuition) ||
  (assert (Cong O P O Y) by finish;intuition ).
  unfold Cong_3.
(* Goal: iff (@Cong Tn A X A B) (@Cong Tn A X A D) *)
  split.
  finish.
  split;finish.
}

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.
(* Goal: @Perp_at Tn R T R R O *)
(* Goal: @Perp Tn A B O T *)
  apply perp_in_comm.
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  assumption.
(* Goal: not (@Col Tn A C P) *)
  intro.
  treat_equalities.
  unfold CongA in H23.
(* Goal: @Le Tn O P O X *)
  tauto.
  induction H10;
(* Goal: @Col Tn Q N Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
  ColR.
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  assumption.
}

(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply tangency_chara; auto.
exists V.
(* Goal: and (@Le Tn O P O X) (not (@Cong Tn O P O X)) *)
(* Goal: forall (_ : @Tangent Tn A B O P) (X : @Tpoint Tn) (_ : @Col Tn A B X), @OutCircle Tn X O P *)
split; auto.
(* Goal: @Cong Tn O P O T' *)
apply per_perp_in in H24; Cong.
apply perp_in_left_comm.
apply perp_in_sym.
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assumption.
(* Goal: False *)
unfold OnCircle in *.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
treat_equalities; tauto.
(* Goal: not (@Col Tn A C P) *)
intro.
treat_equalities.
unfold CongA in H23.
(* Goal: @Le Tn O P O X *)
tauto.
Qed.

Lemma interccat__ncol : forall A B C D P Q,
 InterCCAt A B C D P Q -> ~ Col A C P.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: not (@Col Tn A C P) *)
intro.
(* Goal: False *)
assert (HH := H).
(* Goal: False *)
unfold InterCCAt in HH.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: False *)
apply H2.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply (l4_18 A C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply interccat__neq in H.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
auto.
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assumption.
(* Goal: @Cong Tn O P O T' *)
apply cong_transitivity with A B; Cong.
(* Goal: @Cong Tn O P O T' *)
apply cong_transitivity with C D; Cong.
Qed.

(** Euclid Book III Prop 10
 A circle does not cut a circle at more than two points.
 *)
Lemma cop_onc2__oreq : forall A B C D P Q,
 InterCCAt A B C D P Q -> Coplanar A C P Q ->
 forall Z, OnCircle Z A B -> OnCircle Z C D -> Coplanar A C P Z -> Z=P \/ Z=Q.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
assert(HIC := H).
(* Goal: or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
unfold InterCCAt in H.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
induction (eq_dec_points Z Q).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
  right; auto.
(* Goal: or (and (@Col Tn Q A M) (@Col Tn C M M)) (or (and (@Col Tn Q C M) (@Col Tn A M M)) (and (@Col Tn Q M M) (@Col Tn A C M))) *)
(* Goal: @Coplanar Tn Q A C M *)
(* Goal: not (@eq (@Tpoint Tn) Q M) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
left.
(* Goal: @eq (@Tpoint Tn) Z P *)
assert(HH:=midpoint_existence Q P).
(* Goal: @eq (@Tpoint Tn) Z P *)
ex_and HH M.
(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Per A M Q).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply(mid_onc2__per A B Q P M); auto.
(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Per C M Q).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply(mid_onc2__per C D Q P M); auto.

(* Goal: @eq (@Tpoint Tn) Z P *)
assert(HH:=midpoint_existence Z Q).
(* Goal: @eq (@Tpoint Tn) Z P *)
ex_and HH N.

(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Per A N Q).
(* Goal: @Per Tn A N Q *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply(mid_onc2__per A Z Q Z).
(* Goal: @Cong Tn O P O T' *)
apply cong_transitivity with A B; Cong.
(* Goal: @OnCircle Tn Z C Z *)
(* Goal: @Midpoint Tn N Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Circle.
(* Goal: @Midpoint Tn N Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Midpoint.


(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Per C N Q).
(* Goal: @Per Tn C N Q *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply(mid_onc2__per C Z Q Z).
(* Goal: @Cong Tn O P O T' *)
apply cong_transitivity with C D; Cong.
(* Goal: @OnCircle Tn Z C Z *)
(* Goal: @Midpoint Tn N Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Circle.
(* Goal: @Midpoint Tn N Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Midpoint.

(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Col A C M).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply cop_per2__col with Q; auto.
(* Goal: @Coplanar Tn Q A C M *)
(* Goal: not (@eq (@Tpoint Tn) Q M) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
induction(col_dec P Q A).
(* Goal: @Coplanar Tn Q A C M *)
(* Goal: @Coplanar Tn Q A C M *)
(* Goal: not (@eq (@Tpoint Tn) Q M) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
exists M.
(* Goal: or (and (@Col Tn Q A M) (@Col Tn C M M)) (or (and (@Col Tn Q C M) (@Col Tn A M M)) (and (@Col Tn Q M M) (@Col Tn A C M))) *)
(* Goal: @Coplanar Tn Q A C M *)
(* Goal: not (@eq (@Tpoint Tn) Q M) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
left.
(* Goal: @Col Tn Q N Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
split; ColR.
(* Goal: @Coplanar Tn Q A C M *)
(* Goal: not (@eq (@Tpoint Tn) Q M) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply coplanar_perm_12, col_cop__cop with P; Col; Cop.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assert_diffs;auto.

(* Goal: @eq (@Tpoint Tn) Z P *)
assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply(interccat__neq A B C D P Q); auto.

(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Col A C N).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply cop_per2__col with Q; auto.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply coplanar_perm_12, col_cop__cop with Z; Col.
(* Goal: @Coplanar Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply coplanar_trans_1 with P; Cop.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply interccat__ncol in HIC.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assert_diffs;auto.

(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Perp A C Q P).
(* Goal: @Perp Tn A C Q P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
induction(eq_dec_points A M).
(* Goal: @Perp Tn A C Q P *)
(* Goal: @Perp Tn A C Q P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
subst M.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply per_perp_in in H12; auto.
(* Goal: @Perp Tn A C Q P *)
(* Goal: not (@eq (@Tpoint Tn) A Q) *)
(* Goal: @Perp Tn A C Q P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_in_comm in H12.

(* Goal: @Perp Tn A C Q P *)
(* Goal: not (@eq (@Tpoint Tn) A Q) *)
(* Goal: @Perp Tn A C Q P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_in_perp in H12.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) A Q) *)
(* Goal: @Perp Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_sym.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply (perp_col Q A A C P); Perp.
(* Goal: @Col Tn Q N Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
ColR.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assert_diffs;auto.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply per_perp_in in H11; auto.
(* Goal: @Perp Tn A C Q P *)
(* Goal: not (@eq (@Tpoint Tn) M Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_in_comm in H11.
(* Goal: @Perp Tn A C Q P *)
(* Goal: not (@eq (@Tpoint Tn) M Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_in_perp in H11.
(* Goal: @Perp Tn A C Q P *)
(* Goal: not (@eq (@Tpoint Tn) M Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_comm in H11.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply (perp_col A M M Q C) in H11; Col.
(* Goal: @Perp Tn A C Q P *)
(* Goal: not (@eq (@Tpoint Tn) M Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_sym in H11.
(* Goal: @Perp Tn A C Q P *)
(* Goal: not (@eq (@Tpoint Tn) M Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_comm in H11.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply (perp_col Q M C A P) in H11; Col.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Perp.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assert_diffs;auto.

(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Col Q N Z).
(* Goal: @Col Tn Q N Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
ColR.

(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Perp A C Q Z).
(* Goal: @Perp Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
induction(eq_dec_points A N).
(* Goal: @Perp Tn A C Q Z *)
(* Goal: @Perp Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
subst N.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply per_perp_in in H15; auto.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) A Q) *)
(* Goal: @Perp Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_in_comm in H15.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) A Q) *)
(* Goal: @Perp Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_in_perp in H15.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) A Q) *)
(* Goal: @Perp Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_sym.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply (perp_col Q A A C Z); Perp.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assert_diffs;auto.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply per_perp_in in H14; auto.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_in_comm in H14.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_in_perp in H14.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_comm in H14.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply (perp_col A N N Q C) in H14; Col.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_sym in H14.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_comm in H14.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply (perp_col Q N C A Z) in H14; Col.
(* Goal: @Perp Tn A C Q Z *)
(* Goal: not (@eq (@Tpoint Tn) N Q) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Perp.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
assert_diffs;auto.

(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_sym in H21.
(* Goal: @eq (@Tpoint Tn) Z P *)
apply perp_sym in H19.
(* Goal: @eq (@Tpoint Tn) Z P *)
assert (HH : Par Q P Q Z).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply (l12_9 _ _ _ _ A C); auto.
(* Goal: @Coplanar Tn A C Q Q *)
(* Goal: @Coplanar Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Cop.
(* Goal: @Coplanar Tn A C Q Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply coplanar_trans_1 with P; Cop.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply interccat__ncol in HIC.
(* Goal: not (@Col Tn P A C) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
Col.
(* Goal: @eq (@Tpoint Tn) Z P *)
induction HH.
(* Goal: @eq (@Tpoint Tn) Z P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
unfold Par_strict in H22.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @eq (@Tpoint Tn) Z P *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply False_ind.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) Z P *)
apply H25.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X Q P) (@Col Tn X Q Z)) *)
(* Goal: @eq (@Tpoint Tn) Z P *)
exists Q.
(* Goal: @Col Tn Q N Z *)
(* Goal: @eq (@Tpoint Tn) Z P *)
split; ColR.
(* Goal: @eq (@Tpoint Tn) Z P *)
spliter.
(* Goal: @eq (@Tpoint Tn) Z P *)
assert(Z = P \/ Z = Q).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply(line_circle_two_points A B P Q Z H4); auto.
(* Goal: @Le Tn O P O X *)
induction H26; tauto.
Qed.

End Tangency.

Section Tangency_2D.

Context `{T2D:Tarski_2D}.

Lemma onc2__oreq : forall A B C D P Q,
 InterCCAt A B C D P Q ->
 forall Z, OnCircle Z A B -> OnCircle Z C D  -> Z=P \/ Z=Q.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @InterCCAt Tn A B C D P Q) (Z : @Tpoint Tn) (_ : @OnCircle Tn Z A B) (_ : @OnCircle Tn Z C D), or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
intros.
(* Goal: or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
assert(HCop := all_coplanar A C P Q).
(* Goal: or (@eq (@Tpoint Tn) Z P) (@eq (@Tpoint Tn) Z Q) *)
assert(HCop1 := all_coplanar A C P Z).
(* Goal: @Col Tn A C P *)
(* Goal: @Cong Tn A P A Q *)
(* Goal: @Cong Tn C P C Q *)
apply(cop_onc2__oreq A B C D); assumption.
Qed.

End Tangency_2D.