Require Export GeoCoq.Tarski_dev.Ch12_parallel.

Section Circle.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma inc112 : forall A B,
 InCircle A A B.
Proof.
(* Goal: forall A B : @Tpoint Tn, @InCircle Tn A A B *)
  unfold InCircle.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @Lt Tn A B A P), @Le Tn A B A P *)
  Le.
Qed.

Lemma onc212 : forall A B,
 OnCircle B A B.
Proof.
(* Goal: @OnCircle Tn Q O P *)
(* Goal: @Out Tn O X Q *)
  unfold OnCircle.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  Cong.
Qed.

Lemma onc_sym : forall A B P, OnCircle P A B -> OnCircle B A P.
Proof.
(* Goal: @OnCircle Tn Q O P *)
(* Goal: @Out Tn O X Q *)
  unfold OnCircle.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  Cong.
Qed.

Lemma ninc__outcs : forall X O P, ~ InCircle X O P -> OutCircleS X O P.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @OutCircleS Tn Q O O *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @OutCircleS Tn Q O P) *)
unfold OutCircleS.
(* Goal: @Le Tn U V A B *)
unfold InCircle in *.
(* Goal: @Lt Tn O P O X *)
apply nle__lt in H; auto.
Qed.

Lemma inc__outc : forall A B P, InCircle P A B <-> OutCircle B A P.
Proof.
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
  split; trivial.
Qed.

Lemma incs__outcs : forall A B P, InCircleS P A B <-> OutCircleS B A P.
Proof.
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
  split; trivial.
Qed.

Lemma onc__inc : forall A B P, OnCircle P A B -> InCircle P A B.
Proof.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @OnCircle Tn P A B), @InCircle Tn P A B *)
unfold OnCircle, InCircle.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @Lt Tn A B A P), @Le Tn A B A P *)
Le.
Qed.

Lemma onc__outc : forall A B P, OnCircle P A B -> OutCircle P A B.
Proof.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @OnCircle Tn P A B), @OutCircle Tn P A B *)
unfold OnCircle, OutCircle.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @Lt Tn A B A P), @Le Tn A B A P *)
Le.
Qed.

Lemma inc_outc__onc : forall A B P, InCircle P A B -> OutCircle P A B -> OnCircle P A B.
Proof.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @InCircle Tn P A B) (_ : @OutCircle Tn P A B), @OnCircle Tn P A B *)
  intros A B P HIn HOut.
(* Goal: @OnCircle Tn P A B *)
  apply le_anti_symmetry; trivial.
Qed.

Lemma incs__inc : forall A B P, InCircleS P A B -> InCircle P A B.
Proof.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @InCircleS Tn P A B), @InCircle Tn P A B *)
unfold InCircleS, InCircle.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @Lt Tn A B A P), @Le Tn A B A P *)
Le.
Qed.

Lemma outcs__outc : forall A B P, OutCircleS P A B -> OutCircle P A B.
Proof.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @OutCircleS Tn P A B), @OutCircle Tn P A B *)
unfold OutCircleS, OutCircle.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @Lt Tn A B A P), @Le Tn A B A P *)
Le.
Qed.

Lemma incs__noutc : forall A B P, InCircleS P A B <-> ~ OutCircle P A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: iff (@OutCircleS Tn P A B) (not (@InCircle Tn P A B)) *)
split; intro; [apply lt__nle|apply nle__lt]; assumption.
Qed.

Lemma outcs__ninc : forall A B P, OutCircleS P A B <-> ~ InCircle P A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: iff (@OutCircleS Tn P A B) (not (@InCircle Tn P A B)) *)
split; intro; [apply lt__nle|apply nle__lt]; assumption.
Qed.

Lemma inc__noutcs : forall A B P, InCircle P A B <-> ~ OutCircleS P A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: iff (@OutCircle Tn P A B) (not (@InCircleS Tn P A B)) *)
split; intro; [apply le__nlt|apply nlt__le]; assumption.
Qed.

Lemma outc__nincs : forall A B P, OutCircle P A B <-> ~ InCircleS P A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: iff (@OutCircle Tn P A B) (not (@InCircleS Tn P A B)) *)
split; intro; [apply le__nlt|apply nlt__le]; assumption.
Qed.

Lemma inc_eq : forall A P, InCircle P A A -> A = P.
Proof.
(* Goal: forall (A P : @Tpoint Tn) (_ : @InCircle Tn P A A), @eq (@Tpoint Tn) A P *)
intros A B HIn.
(* Goal: @eq (@Tpoint Tn) A B *)
apply le_zero with A; assumption.
Qed.

Lemma outc_eq : forall A B, OutCircle A A B -> A = B.
Proof.
(* Goal: forall (A B : @Tpoint Tn) (_ : @OutCircle Tn A A B), @eq (@Tpoint Tn) A B *)
intros A B HOut.
(* Goal: @eq (@Tpoint Tn) A B *)
apply le_zero with A; assumption.
Qed.

Lemma onc2__cong : forall O P A B, OnCircle A O P -> OnCircle B O P -> Cong O A O B.
Proof.
(* Goal: @OnCircle Tn Q O P *)
(* Goal: @Out Tn O X Q *)
unfold OnCircle.
(* Goal: forall (O P A B : @Tpoint Tn) (_ : @Cong Tn O A O P) (_ : @Cong Tn O B O P), @Cong Tn O A O B *)
intros O P A B H1 H2.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
Qed.

End Circle.


Hint Resolve inc112 onc212 onc_sym inc__outc onc__inc onc__outc
             inc_outc__onc incs__inc outcs__outc : circle.

Ltac Circle := auto with circle.

Ltac treat_equalities :=
try treat_equalities_aux;
repeat
  match goal with
   | H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
      apply cong_symmetry in H; apply cong_identity in H;
      smart_subst X2;clean_reap_hyps
   | H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
      apply cong_identity in H;smart_subst X2;clean_reap_hyps
   | H:(Bet ?X1 ?X2 ?X1) |- _ =>
      apply  between_identity in H;smart_subst X2;clean_reap_hyps
   | H:(Midpoint ?X ?Y ?Y) |- _ => apply l7_3 in H; smart_subst Y;clean_reap_hyps
   | H : Bet ?A ?B ?C, H2 : Bet ?B ?A ?C |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T : A=B) by (apply (between_equality A B C); finish);
                       smart_subst A;clean_reap_hyps
   | H : Bet ?A ?B ?C, H2 : Bet ?A ?C ?B |- _ =>
     let T := fresh in not_exist_hyp (B=C); assert (T : B=C) by (apply (between_equality_2 A B C); finish);
                       smart_subst B;clean_reap_hyps
   | H : Bet ?A ?B ?C, H2 : Bet ?C ?A ?B |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T : A=B) by (apply (between_equality A B C); finish);
                       smart_subst A;clean_reap_hyps
   | H : Bet ?A ?B ?C, H2 : Bet ?B ?C ?A |- _ =>
     let T := fresh in not_exist_hyp (B=C); assert (T : B=C) by (apply (between_equality_2 A B C); finish);
                       smart_subst A;clean_reap_hyps
   | H:(Le ?X1 ?X2 ?X3 ?X3) |- _ =>
      apply le_zero in H;smart_subst X2;clean_reap_hyps
   | H : Midpoint ?P ?A ?P1, H2 : Midpoint ?P ?A ?P2 |- _ =>
     let T := fresh in not_exist_hyp (P1=P2);
                      assert (T := symmetric_point_uniqueness A P P1 P2 H H2);
                      smart_subst P1;clean_reap_hyps
   | H : Midpoint ?A ?P ?X, H2 : Midpoint ?A ?Q ?X |- _ =>
     let T := fresh in not_exist_hyp (P=Q); assert (T := l7_9 P Q A X H H2);
                       smart_subst P;clean_reap_hyps
   | H : Midpoint ?A ?P ?X, H2 : Midpoint ?A ?X ?Q |- _ =>
     let T := fresh in not_exist_hyp (P=Q); assert (T := l7_9_bis P Q A X H H2);
                       smart_subst P;clean_reap_hyps
   | H : Midpoint ?M ?A ?A |- _ =>
     let T := fresh in not_exist_hyp (M=A); assert (T : l7_3 M A H);
                       smart_subst M;clean_reap_hyps
   | H : Midpoint ?A ?P ?P', H2 : Midpoint ?B ?P ?P' |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := l7_17 P P' A B H H2);
                       smart_subst A;clean_reap_hyps
   | H : Midpoint ?A ?P ?P', H2 : Midpoint ?B ?P' ?P |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := l7_17_bis P P' A B H H2);
                       smart_subst A;clean_reap_hyps
   | H : Midpoint ?A ?B ?A |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id_2 A B H);
                       smart_subst A;clean_reap_hyps
   | H : Midpoint ?A ?A ?B |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id A B H);
                       smart_subst A;clean_reap_hyps
   | H : OnCircle ?A ?A ?B |- _ =>
      apply cong_reverse_identity in H;smart_subst B;clean_reap_hyps
   | H : OnCircle ?B ?A ?A |- _ =>
      apply cong_identity in H;smart_subst B;clean_reap_hyps
   | H : InCircle ?B ?A ?A |- _ =>
      apply le_zero in H;smart_subst B;clean_reap_hyps
   | H : OutCircle ?A ?A ?B |- _ =>
      apply le_zero in H;smart_subst B;clean_reap_hyps
end.

Section Circle_2.


Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** If a point is strictly inside a segment of a disk, it is strictly inside the circle. *)

Lemma bet_inc2__incs : forall O P U V X,
 X <> U -> X <> V -> Bet U X V ->
 InCircle U O P -> InCircle V O P ->
 InCircleS X O P.
Proof.
(* Goal: forall (O P U V X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) X U)) (_ : not (@eq (@Tpoint Tn) X V)) (_ : @Bet Tn U X V) (_ : @InCircle Tn U O P) (_ : @InCircle Tn V O P), @InCircleS Tn X O P *)
intros O P U V X HUX HVX HBet HUIn HVIn.
(* Goal: @InCircleS Tn X O P *)
destruct (le_cases O U O V).
- apply le3456_lt__lt with O V; trivial.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @Lt Tn A B A P), @Le Tn A B A P *)
  apply lt_comm, (bet_le__lt U); Le.
- apply le3456_lt__lt with O U; trivial.
(* Goal: forall (A B P : @Tpoint Tn) (_ : @Lt Tn A B A P), @Le Tn A B A P *)
  apply lt_comm, (bet_le__lt V); Between; Le.
Qed.

Lemma bet_incs2__incs : forall O P U V X,
 Bet U X V -> InCircleS U O P -> InCircleS V O P ->
 InCircleS X O P.
Proof.
(* Goal: forall (O P U V X : @Tpoint Tn) (_ : @Bet Tn U X V) (_ : @InCircleS Tn U O P) (_ : @InCircleS Tn V O P), @InCircleS Tn X O P *)
intros O P U V X HBet HUIn HVIn.
(* Goal: @InCircleS Tn X O P *)
destruct (eq_dec_points X U).
(* Goal: @Cong Tn C Z C I *)
(* Goal: @Cong Tn C Z C I *)
  subst; assumption.
(* Goal: @InCircleS Tn X O P *)
destruct (eq_dec_points X V).
(* Goal: @Cong Tn C Z C I *)
(* Goal: @Cong Tn C Z C I *)
  subst; assumption.
(* Goal: @InCircleS Tn X O P *)
apply bet_inc2__incs with U V; Circle.
Qed.

(** If A and B are two points inside the circle, then all points on the segment AB are also
    in the circle, i.e. a circle is a convex figure.
*)

Lemma bet_inc2__inc : forall A B U V P, InCircle U A B -> InCircle V A B -> Bet U P V ->
  InCircle P A B.
Proof.
(* Goal: forall (A B U V P : @Tpoint Tn) (_ : @InCircle Tn U A B) (_ : @InCircle Tn V A B) (_ : @Bet Tn U P V), @InCircle Tn P A B *)
  intros A B U V P HU HV HBet.
(* Goal: @InCircle Tn P A B *)
  destruct (eq_dec_points P U).
(* Goal: @InCircle Tn P A B *)
(* Goal: @InCircle Tn P A B *)
    subst P; assumption.
(* Goal: @InCircle Tn P A B *)
  destruct (eq_dec_points P V).
(* Goal: @InCircle Tn P A B *)
(* Goal: @InCircle Tn P A B *)
    subst P; assumption.
(* Goal: @InCircle Tn P A B *)
  apply incs__inc, bet_inc2__incs with U V; assumption.
Qed.

(** Given two points U and V on a circle, the points of the line UV which are inside the circle are
    between U and V. *) 

Lemma col_inc_onc2__bet : forall A B U V P, U <> V -> OnCircle U A B -> OnCircle V A B ->
  Col U V P -> InCircle P A B -> Bet U P V.
Proof.
(* Goal: forall (A B U V P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) U V)) (_ : @OnCircle Tn U A B) (_ : @OnCircle Tn V A B) (_ : @Col Tn U V P) (_ : @InCircle Tn P A B), @Bet Tn U P V *)
  intros A B U V P HUV HU HV HCol HIn.
(* Goal: @Bet Tn U P V *)
  assert (Cong A U A V) by (apply cong_transitivity with A B; Cong).
(* Goal: @Bet Tn U P V *)
  destruct HCol as [HBet|[HBet|HBet]]; Between.
  - destruct (eq_dec_points P V); try (subst; Between).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X A B) (not (@OnCircle Tn X C D))) *)
    exfalso.
(* Goal: False *)
    assert (HLt : Lt V A U A).
(* Goal: @Lt Tn V A U A *)
(* Goal: False *)
      apply (bet_le__lt P); Between.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
      apply (l5_6 A P A B); Cong.
(* Goal: False *)
    destruct HLt as [HLe HNCong].
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
    apply HNCong; Cong.
  - destruct (eq_dec_points P U); try (subst; Between).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X A B) (not (@OnCircle Tn X C D))) *)
    exfalso.
(* Goal: False *)
    assert (HLt : Lt U A V A).
(* Goal: @Lt Tn U A V A *)
(* Goal: False *)
      apply (bet_le__lt P); trivial.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
      apply (l5_6 A P A B); Cong.
(* Goal: False *)
    destruct HLt as [HLe HNCong].
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
    apply HNCong; Cong.
Qed.

(** Given two points U and V on a circle, all points of line UV which are outside the segment UV are
    outside the circle. *)

Lemma onc2_out__outcs : forall A B U V P, U <> V -> OnCircle U A B -> OnCircle V A B -> Out P U V ->
  OutCircleS P A B.
Proof.
(* Goal: forall (A B U V P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) U V)) (_ : @OnCircle Tn U A B) (_ : @OnCircle Tn V A B) (_ : @Out Tn P U V), @OutCircleS Tn P A B *)
  intros A B U V P HUV HUOn HVOn HOut.
(* Goal: @OutCircleS Tn P A B *)
  apply outcs__ninc.
(* Goal: not (@InCircle Tn P A B) *)
  intro HIn.
(* Goal: False *)
  apply (not_bet_and_out U P V).
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
  split; trivial.
(* Goal: @Bet Tn U P V *)
  apply (col_inc_onc2__bet A B); Col.
Qed.

(** Given two points U and V inside a circle, all points of line UV which are outside the circle are
    outside the segment UV. *)

Lemma col_inc2_outcs__out : forall A B U V P, InCircle U A B -> InCircle V A B ->
  Col U V P -> OutCircleS P A B -> Out P U V.
Proof.
(* Goal: forall (A B U V P : @Tpoint Tn) (_ : @InCircle Tn U A B) (_ : @InCircle Tn V A B) (_ : @Col Tn U V P) (_ : @OutCircleS Tn P A B), @Out Tn P U V *)
  intros A B U V P HUIn HVIn HCol HOut.
(* Goal: @Out Tn P U V *)
  apply not_bet_out; Col.
(* Goal: not (@Bet Tn U P V) *)
  intro HBet.
(* Goal: False *)
  apply outcs__ninc in HOut.
(* Goal: False *)
  apply HOut, bet_inc2__inc with U V; trivial.
Qed.

(** If the center of a circle belongs to a chord, then it is the midpoint of the chord. *)

Lemma col_onc2__mid : forall A B U V, U <> V -> OnCircle U A B -> OnCircle V A B ->
  Col U V A -> Midpoint A U V.
Proof.
(* Goal: forall (A B U V : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) U V)) (_ : @OnCircle Tn U A B) (_ : @OnCircle Tn V A B) (_ : @Col Tn U V A), @Midpoint Tn A U V *)
  intros A B U V HUV HU HV HCol.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
  split.
(* Goal: @Bet Tn U A V *)
(* Goal: @Cong Tn U A A V *)
    apply (col_inc_onc2__bet A B); Circle.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
    apply cong_transitivity with A B; Cong.
Qed.

(** Given a point U on a circle and a point P inside the circle, there is a point V such as
    UV is a chord of the circle going through P. *)

Lemma chord_completion : forall A B U P, OnCircle U A B -> InCircle P A B ->
  exists V, OnCircle V A B /\ Bet U P V.
Proof.
(* Goal: forall (A B U P : @Tpoint Tn) (_ : @OnCircle Tn U A B) (_ : @InCircle Tn P A B), @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
  intros A B U P HOn HIn.
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
  destruct (eq_dec_points U A).
    unfold OnCircle, InCircle in *|-.
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
    treat_equalities; exists U; split; Circle; Between.
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
  assert (HA' : exists A', U <> A' /\ Col U P A' /\ Per A A' U).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
  { destruct (col_dec U P A) as [HCol|HNCol].
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) U A')) (and (@Col Tn U P A') (@Per Tn A A' U))) *)
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) U A')) (and (@Col Tn U P A') (@Per Tn A A' U))) *)
      exists A; split; Col; Perp.
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) U A')) (and (@Col Tn U P A') (@Per Tn A A' U))) *)
    destruct (l8_18_existence U P A) as [A' [HCol HPerp]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) U A')) (and (@Col Tn U P A') (@Per Tn A A' U))) *)
    assert (U <> A').
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
    { intro; treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
      assert_diffs.
(* Goal: False *)
      destruct (l11_46 P U A) as [_ HLt]; auto.
(* Goal: or (@Per Tn P U A) (@Obtuse Tn P U A) *)
(* Goal: False *)
        left; Perp.
(* Goal: False *)
      apply lt__nle in HLt.
(* Goal: False *)
      apply HLt.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
      apply (l5_6 A P A B); Cong.
    }
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
    exists A'; repeat split; trivial.
(* Goal: @Per Tn A A' U *)
    apply l8_2, perp_per_1.
(* Goal: @Perp Tn A' U A A' *)
    apply perp_left_comm, perp_col with P; trivial.
  }
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
  destruct HA' as [A' [HUA' [HCol HPer]]].
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
  destruct (symmetric_point_construction U A') as [V HV].
(* Goal: not (@eq (@Tpoint Tn) M U) *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
  assert (HCong := per_double_cong A A' U V HPer HV).
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@OnCircle Tn V A B) (@Bet Tn U P V)) *)
  assert (HVOn : OnCircle V A B).
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
    unfold OnCircle in *.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
    apply cong_transitivity with A U; Cong.
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
  exists V; split; trivial.
(* Goal: @Bet Tn U P V *)
  apply (col_inc_onc2__bet A B); trivial.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
  ColR.
Qed.

(** Given a circle, there is a point strictly outside the circle. *)

Lemma outcs_exists : forall O P, exists Q, OutCircleS Q O P.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction(eq_dec_points O P).
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
subst P.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @OutCircleS Tn Q O O) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @OutCircleS Tn Q O P) *)
assert(HH:=another_point O).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@OnCircle Tn Q O P) (@Out Tn O X Q)) *)
ex_and HH Q.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@OnCircle Tn Q O P) (@Out Tn O X Q)) *)
exists Q.
(* Goal: @OutCircleS Tn Q O O *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @OutCircleS Tn Q O P) *)
unfold OutCircleS.
(* Goal: @InCircleS Tn O O P *)
apply lt1123;auto.

(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @OutCircleS Tn Q O P) *)
assert(HH:=segment_construction O P O P).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@OnCircle Tn Q O P) (@Out Tn O X Q)) *)
ex_and HH Q.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@OnCircle Tn Q O P) (@Out Tn O X Q)) *)
exists Q.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
(* Goal: @Le Tn O P O Q *)
(* Goal: not (@Cong Tn O P O Q) *)
exists P.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
split; Cong.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: False *)
assert (P=Q) by eauto using between_cong.
(* Goal: False *)
treat_equalities;intuition.
Qed.

(** Given a circle of center O and a ray OX, there is a point on the ray
    which is also strictly outside the circle. *)

Lemma outcs_exists1 : forall O P X, X <> O -> exists Q, Out O X Q /\ OutCircleS Q O P.
Proof.
(* Goal: forall (O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) X O)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Out Tn O X Q) (@OutCircleS Tn Q O P)) *)
intros O P X HOX.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Out Tn O X Q) (@OutCircleS Tn Q O P)) *)
destruct (segment_construction O X O P) as [Q [HQ1 HQ2]].
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
exists Q; split.
(* Goal: @Out Tn O X Q *)
(* Goal: @OutCircleS Tn Q O P *)
  apply bet_out; auto.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
- apply le_comm.
(* Goal: @Le Tn P O Q O *)
  exists X.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  split; Between; Cong.
- intro.
(* Goal: False *)
  apply HOX.
(* Goal: @eq (@Tpoint Tn) X O *)
  apply between_cong with Q; Between.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply cong_transitivity with O P; Cong.
Qed.

(** Given a circle there is a point which is strictly inside. *)

Lemma incs_exists : forall O P, O <> P -> exists Q, InCircleS Q O P.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @InCircleS Tn Q O P) *)
exists O.
(* Goal: @InCircleS Tn O O P *)
apply lt1123;auto.
Qed.

(** Given a circle of center O and a ray OX, there is a point on the ray
    which is also strictly inside the circle. *)

Lemma incs_exists1 : forall O P X, X <> O -> P <> O -> exists Q, Out O X Q /\ InCircleS Q O P.
Proof.
(* Goal: forall (O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) X O)) (_ : not (@eq (@Tpoint Tn) P O)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Out Tn O X Q) (@InCircleS Tn Q O P)) *)
intros O P X HOX HOP.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Out Tn O X Q) (@InCircleS Tn Q O P)) *)
destruct (midpoint_existence O P) as [M HM].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Out Tn O X Q) (@InCircleS Tn Q O P)) *)
destruct (segment_construction_3 O X O M) as [Q [HQ1 HQ2]]; auto.
(* Goal: not (@eq (@Tpoint Tn) C1 O) *)
(* Goal: not (@eq (@Tpoint Tn) C1 I) *)
  intro; treat_equalities; auto.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Out Tn O X Q) (@InCircleS Tn Q O P)) *)
exists Q; split; auto.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply (cong2_lt__lt O M O P); Cong.
(* Goal: @Lt Tn O M O P *)
apply mid__lt; auto.
Qed.

(** Given a circle of center O and a ray OX, there is a point on the ray which is also on the circle. *)

Lemma onc_exists : forall O P X,  X <> O -> O <> P -> exists Q, OnCircle Q O P /\ Out O X Q.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@OnCircle Tn Q O P) (@Out Tn O X Q)) *)
assert(HH:=segment_construction_2 X O O P H).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@OnCircle Tn Q O P) (@Out Tn O X Q)) *)
ex_and HH Q.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@OnCircle Tn Q O P) (@Out Tn O X Q)) *)
exists Q.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
(* Goal: @OnCircle Tn Q O P *)
(* Goal: @Out Tn O X Q *)
unfold OnCircle.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
Cong.
(* Goal: @Out Tn T O A *)
unfold Out.
(* Goal: and (not (@eq (@Tpoint Tn) O T)) (and (not (@eq (@Tpoint Tn) A T)) (or (@Bet Tn T O A) (@Bet Tn T A O))) *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
subst Q.
(* Goal: False *)
treat_equalities; tauto.
Qed.

(** Given a circle of center O and a line OX, O is between two points of the line
    which are also on the circle. *)

Lemma diam_points : forall O P X, exists Q1 Q2,
  Bet Q1 O Q2 /\ Col Q1 Q2 X /\ OnCircle Q1 O P /\ OnCircle Q2 O P.
Proof.
(* Goal: forall O P X : @Tpoint Tn, or (@OnCircle Tn X O P) (or (@InCircleS Tn X O P) (@OutCircleS Tn X O P)) *)
intros O P X.
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
destruct (eq_dec_points X O).
(* Goal: @eq (@Tpoint Tn) O X *)
(* Goal: @eq (@Tpoint Tn) O X *)
  subst X.
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 O) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
  destruct (segment_construction P O O P) as [P' [HP'1 HP'2]].
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 O) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
  exists P, P'; repeat split; Col; Circle.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
destruct (eq_dec_points O P).
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
  subst P.
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O O) (@OnCircle Tn Q2 O O))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
  exists O, O; repeat split; finish; Circle.
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
assert(HH:= onc_exists O P X H H0).
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
ex_and HH Q1.
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
assert(HH:= segment_construction Q1 O O Q1).
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
ex_and HH Q2.
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
exists Q1, Q2.
(* Goal: and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))) *)
repeat split; Col.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
ColR.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O Q1; Cong.
Qed.

(** The symmetric of a point on a circle relative to the center is also on the circle. *)

Lemma symmetric_oncircle : forall X Y O P, 
 Midpoint O X Y -> OnCircle X O P -> OnCircle Y O P.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O X; Cong.
Qed.


(** The middle of a chord together with the center of the circle and one end of the chord
    form a right angle *)

Lemma mid_onc2__per : forall O P U V X,
 OnCircle U O P -> OnCircle V O P -> Midpoint X U V -> Per O X U.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Per Tn A M X *)
unfold Per.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn M U C') (@Cong Tn X U X C')) *)
(* Goal: @Col Tn O X M *)
exists V.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
split; trivial.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
Qed.

(** Euclid Book III Prop 3 (two lemmas).
 If a straight line passing through the center of a circle 
 bisects a straight line not passing through the center,
 then it also cuts it at right angles; and if it cuts it at right angles, then it also bisects it.
*)

(** The line from the center of a circle to the midpoint of a chord is perpendicular to the chord. *)

Lemma mid_onc2__perp : forall O P A B X,
 O <> X -> A <> B -> OnCircle A O P -> OnCircle B O P -> Midpoint X A B -> Perp O X A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Perp Tn O X A B *)
assert(Per O X A).
(* Goal: @Per Tn O X A *)
(* Goal: @Perp Tn O X A B *)
apply (mid_onc2__per O P A B X); auto.
(* Goal: @Perp Tn O A Y X *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.

(* Goal: @Perp Tn O X A B *)
apply per_perp_in in H4; auto.
(* Goal: @Perp Tn O X A B *)
(* Goal: not (@eq (@Tpoint Tn) X A) *)
apply perp_in_perp in H4.
(* Goal: @Perp Tn O X A B *)
(* Goal: not (@eq (@Tpoint Tn) X A) *)
apply perp_sym.

(* Goal: @Perp Tn A B O X *)
(* Goal: not (@eq (@Tpoint Tn) X A) *)
apply (perp_col _ X); Perp.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
Col.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: @eq (@Tpoint Tn) O X *)
(* Goal: @eq (@Tpoint Tn) O X *)
subst X.
(* Goal: False *)
treat_equalities; tauto.
Qed.

(** If a line passing through the center of a circle is perpendicular to a chord,
    then they intersect at the middle of the chord *)

Lemma col_onc2_perp__mid : forall O P A B X,
 O<>X -> A<>B -> Col A B X -> OnCircle A O P -> OnCircle B O P -> Perp O X A B -> Midpoint X A B.
Proof.
(* Goal: forall (O P A B X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) O X)) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Col Tn A B X) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @Perp Tn O X A B), @Midpoint Tn X A B *)
  intros O P A B X HOX HAB HCol HAOn HBOn HPerp.
(* Goal: @Midpoint Tn X A B *)
  destruct (midpoint_existence A B) as [M HM].
(* Goal: @Midpoint Tn X A B *)
  cut (X = M).
(* Goal: forall _ : @eq (@Tpoint Tn) X M, @Midpoint Tn X A B *)
(* Goal: @eq (@Tpoint Tn) X M *)
    intro; subst; trivial.
(* Goal: @eq (@Tpoint Tn) X M *)
  assert (HNCol : ~ Col A B O) by (destruct (perp_not_col2 A B O X); Perp; Col).
(* Goal: @eq (@Tpoint Tn) X M *)
  apply (l8_18_uniqueness A B O); Col; Perp.
(* Goal: @Perp Tn A B O M *)
  apply perp_sym, mid_onc2__perp with P; auto.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  intro; subst; apply HNCol; Col.
Qed.

(** If two circles intersect at a point which is not on the line joining the center,
    then they intersect on any half-plane delimited by that line. *)

Lemma circle_circle_os : forall A B C D I P,
  OnCircle I A B -> OnCircle I C D -> ~ Col A C I -> ~ Col A C P ->
  exists Z, OnCircle Z A B /\ OnCircle Z C D /\ OS A C P Z.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : @OnCircle Tn I A B) (_ : @OnCircle Tn I C D) (_ : not (@Col Tn A C I)) (_ : not (@Col Tn A C P)), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z))) *)
  intros A B C D I P HI1 HI2 HNCol1 HNCol2.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z))) *)
  destruct (l8_18_existence A C I) as [X []]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z))) *)
  destruct (l10_15 A C X P) as [Z0 []]; trivial.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z))) *)
  destruct (l6_11_existence X X I Z0) as [Z []]; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z))) *)
  exists Z.
(* Goal: and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z)) *)
  assert (Perp A C X Z).
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    assert_diffs; apply perp_sym, perp_col with Z0; Perp; Col.
(* Goal: and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z)) *)
  assert (OS A C P Z).
(* Goal: @OS Tn A C P Z *)
(* Goal: and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z)) *)
    apply one_side_transitivity with Z0; trivial.
(* Goal: @OS Tn A C Z0 Z *)
(* Goal: and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z)) *)
    apply out_one_side_1 with X; [apply one_side_not_col124 with P| |apply l6_6]; trivial.
(* Goal: and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@OS Tn A C P Z)) *)
  clear dependent Z0.
(* Goal: and (not (@eq (@Tpoint Tn) O T)) (and (not (@eq (@Tpoint Tn) A T)) (or (@Bet Tn T O A) (@Bet Tn T A O))) *)
  repeat split; auto.
  - apply cong_transitivity with A I; trivial.
(* Goal: @Cong Tn A Z A I *)
    destruct (eq_dec_points A X).
(* Goal: @Cong Tn C Z C I *)
(* Goal: @Cong Tn C Z C I *)
      subst; assumption.
    apply l10_12 with X X; Cong; [apply perp_per_2|apply perp_per_1];
(* Goal: @eq (@Tpoint Tn) O X *)
      apply perp_left_comm, perp_col with C; auto.
  - apply cong_transitivity with C I; trivial.
(* Goal: @Cong Tn C Z C I *)
    destruct (eq_dec_points C X).
(* Goal: @Cong Tn C Z C I *)
(* Goal: @Cong Tn C Z C I *)
      subst; assumption.
    apply l10_12 with X X; Cong; [apply perp_per_2|apply perp_per_1];
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
      apply perp_left_comm, perp_col with A; Perp; Col.
Qed.

(** If two circles intersect, then they intersect on any plane containing the centers *)

Lemma circle_circle_cop : forall A B C D I P, OnCircle I A B -> OnCircle I C D ->
  exists Z, OnCircle Z A B /\ OnCircle Z C D /\ Coplanar A C P Z.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : @OnCircle Tn I A B) (_ : @OnCircle Tn I C D), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@Coplanar Tn A C P Z))) *)
  intros A B C D I P HI1 HI2.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@Coplanar Tn A C P Z))) *)
  destruct (col_dec A C P).
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
    exists I; repeat split; trivial.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    exists P; left; split; Col.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@Coplanar Tn A C P Z))) *)
  destruct (col_dec A C I).
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
    exists I; repeat split; trivial.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    exists I; left; split; Col.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@Coplanar Tn A C P Z))) *)
  destruct (circle_circle_os A B C D I P) as [Z [HZ1 [HZ2 HOS]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (and (@OnCircle Tn Z C D) (@Coplanar Tn A C P Z))) *)
  exists Z; repeat split; Cop.
Qed.

(** A circle does not cut a line at more than two points. *)

Lemma line_circle_two_points : forall O P U V W,
 U <> V -> Col U V W -> OnCircle U O P -> OnCircle V O P -> OnCircle W O P -> 
 W = U \/ W = V.
Proof.
(* Goal: forall (O P U V W : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) U V)) (_ : @Col Tn U V W) (_ : @OnCircle Tn U O P) (_ : @OnCircle Tn V O P) (_ : @OnCircle Tn W O P), or (@eq (@Tpoint Tn) W U) (@eq (@Tpoint Tn) W V) *)
intros O P U V W HUV HCol HUOn HVOn HWOn.
(* Goal: or (@eq (@Tpoint Tn) W U) (@eq (@Tpoint Tn) W V) *)
destruct (eq_dec_points W U); auto.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
right.
(* Goal: @eq (@Tpoint Tn) W V *)
apply between_equality with U; apply col_inc_onc2__bet with O P; Col; Circle.
Qed.

(** The midpoint of a chord is strictly inside the circle. *)

Lemma onc2_mid__incs : forall O P U V M, 
 U <> V -> OnCircle U O P -> OnCircle V O P -> Midpoint M U V ->
 InCircleS M O P.
Proof.
(* Goal: forall (O P U V M : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) U V)) (_ : @OnCircle Tn U O P) (_ : @OnCircle Tn V O P) (_ : @Midpoint Tn M U V), @InCircleS Tn M O P *)
intros O P U V M HUV HUOn HVOn HM.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
(* Goal: @InCircleS Tn M O P *)
apply bet_inc2__incs with U V; Between; Circle.
Qed.

(** A point is either strictly inside, on or strictly outside a circle. *)

Lemma circle_cases : forall O P X,
  OnCircle X O P \/ InCircleS X O P \/ OutCircleS X O P.
Proof.
(* Goal: forall O P X : @Tpoint Tn, or (@OnCircle Tn X O P) (or (@InCircleS Tn X O P) (@OutCircleS Tn X O P)) *)
intros O P X.
(* Goal: or (@OnCircle Tn X O P) (or (@InCircleS Tn X O P) (@OutCircleS Tn X O P)) *)
destruct (cong_dec O X O P); auto.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
right.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
destruct (le_cases O P O X); [right|left]; split; Cong.
Qed.

(** If a point is inside a circle, then it lies on a radius. *)

Lemma inc__radius : forall O P X, InCircle X O P ->
  exists Y, OnCircle Y O P /\ Bet O X Y.
Proof.
(* Goal: forall (O P X : @Tpoint Tn) (_ : @InCircle Tn X O P), @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
  intros O P X HIn.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
  destruct (eq_dec_points O P).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
    unfold InCircle in HIn; treat_equalities.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O O) (@Bet Tn O O Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
    exists O; split; Circle; Between.
(* Goal: @Col Tn X Y O *)
  destruct (eq_dec_points O X).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
    subst; exists P; split; Circle; Between.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
  destruct (segment_construction_3 O X O P) as [Y [HY1 HY2]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@OnCircle Tn Y O P) (@Bet Tn O X Y)) *)
  exists Y; split; auto.
(* Goal: @Bet Tn O X Y *)
  apply l6_13_1; trivial.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply (l5_6 O X O P); Cong.
Qed.

Lemma onc_not_center : forall O P A, O <> P -> OnCircle A O P -> A <> O.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: False *)
treat_equalities; tauto.
Qed.

Lemma onc2_per__mid : forall O P U V M, U <> V -> M <> U ->
 OnCircle U O P -> OnCircle V O P -> Col M U V -> Per O M U -> Midpoint M U V .
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Midpoint Tn M U V *)
assert(HH:=midpoint_existence U V).
(* Goal: @Midpoint Tn M U V *)
ex_and HH M'.
(* Goal: @Midpoint Tn M U V *)
assert(HH:=(mid_onc2__per O P U V M' H1 H2 H5)).
(* Goal: @Midpoint Tn M U V *)
assert(M = M' \/ ~ Col M' U V).
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(col_per2_cases O M U V M'); Col.
(* Goal: not (@eq (@Tpoint Tn) M' U) *)
(* Goal: @Midpoint Tn M U V *)
assert_diffs;auto.
(* Goal: @Midpoint Tn M U V *)
induction H6.
(* Goal: @Midpoint Tn M U V *)
(* Goal: @Midpoint Tn M U V *)
subst M'.
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
assumption.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: False *)
apply H6.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
ColR.
Qed.

(** Euclid Book III Prop 14
Equal straight lines in a circle are equally distant from the center, 
and those which are equally distant from the center equal one another.
*)

Lemma cong_chord_cong_center : forall O P A B C D M N,
 OnCircle A O P ->
 OnCircle B O P ->
 OnCircle C O P ->
 OnCircle D O P ->
 Midpoint M A B ->
 Midpoint N C D ->
 Cong A B C D ->
 Cong O N O M.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Cong Tn O N O M *)
assert(Cong M B N D).
(* Goal: @Cong Tn O N O M *)
apply cong_commutativity.
(* Goal: @Cong Tn B M D N *)
(* Goal: @Cong Tn O N O M *)
eapply (cong_cong_half_1 _ _ A _ _ C); Midpoint.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
Cong.
(* Goal: @Perp Tn O A Y X *)
unfold Midpoint in *.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @Cong Tn O N O M *)
apply cong_commutativity.
(* Goal: @Cong Tn N O M O *)
apply cong_symmetry.
(* Goal: @Cong Tn M O N O *)
apply(l4_2 A M B O C N D O).
(* Goal: @IFSC Tn A M B O C N D O *)
unfold IFSC.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
repeat split; Cong.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply (cong_transitivity _ _ O P); Cong.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply (cong_transitivity _ _ O P); Cong.
Qed.

(** variant *)
Lemma cong_chord_cong_center1 : forall O P A B C D M N,
 A <> B -> C <> D -> M <> A -> N <> C ->
 OnCircle A O P ->
 OnCircle B O P ->
 OnCircle C O P ->
 OnCircle D O P ->
 Col M A B ->
 Col N C D ->
 Per O M A ->
 Per O N C ->
 Cong A B C D ->
 Cong O N O M.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Cong Tn O N O M *)
assert(Midpoint M A B).
(* Goal: @Midpoint Tn M A B *)
(* Goal: @Cong Tn O N O M *)
apply(onc2_per__mid O P A B M H H1 H3 H4 H7 H9).
(* Goal: @Cong Tn O N O M *)
assert(Midpoint N C D).
(* Goal: @Midpoint Tn N C D *)
(* Goal: @Cong Tn O N O M *)
apply(onc2_per__mid O P C D N H0 H2 H5 H6 H8 H10).
(* Goal: @Cong Tn O N O M *)
apply (cong_chord_cong_center O P A B C D M N); auto.
Qed.

(** Prop 7   **)

Lemma onc_sym__onc : forall O P A B X Y, 
Bet O A B -> OnCircle A O P -> OnCircle B O P -> OnCircle X O P -> ReflectL X Y A B -> OnCircle Y O P.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Cong Tn O Y O P *)
assert(Cong X O Y O).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
  {
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    apply(is_image_spec_col_cong A B X Y O H3);Col.
  }
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O X; Cong.
Qed.


Lemma mid_onc__diam : forall O P A B, OnCircle A O P -> Midpoint O A B -> Diam A B O P.
Proof.
(* Goal: forall (O P A B : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @Midpoint Tn O A B), @Diam Tn A B O P *)
  intros O P A B HA HB.
(* Goal: and (@Bet Tn B O A) (and (@OnCircle Tn B O P) (@OnCircle Tn A O P)) *)
  repeat split; Between.
(* Goal: @OnCircle Tn B O P *)
  apply (symmetric_oncircle A); trivial.
Qed.

Lemma chord_le_diam : forall O P A B U V,
 Diam A B O P -> OnCircle U O P -> OnCircle V O P -> Le U V A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
apply(triangle_inequality_2 U O V A O B); trivial;
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
Qed.

Lemma chord_lt_diam : forall O P A B U V, 
 ~ Col O U V -> Diam A B O P -> OnCircle U O P -> OnCircle V O P ->
 Lt U V A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Lt Tn U V A B *)
assert(HH:= chord_le_diam O P A B U V H0 H1 H2).
(* Goal: @Lt Tn T X T A *)
unfold Lt.
(* Goal: and (@Midpoint Tn M X Y) (@Cong Tn A X A Y) *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: False *)
apply H.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @Col Tn O U V *)
assert(HP:=midpoint_existence U V).
(* Goal: @Col Tn O U V *)
ex_and HP O'.
(* Goal: @Perp Tn O A Y X *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Bet Tn A O B *)
assert(Cong O A O B) by (apply cong_transitivity with O P; Cong).
(* Goal: @Col Tn O U V *)
assert(Cong A O U O').
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply(cong_cong_half_1 A O B U O' V); unfold Midpoint; try split; Cong.
(* Goal: @Col Tn O U V *)
assert(Cong B O V O').
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply(cong_cong_half_2 A O B U O' V); unfold Midpoint; try split; Cong.
(* Goal: @Col Tn O U V *)
apply(l4_13 O A B).
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
Col.
(* Goal: @Cong_3 Tn O A B O U V *)
unfold Cong_3.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
repeat split; Cong; apply cong_transitivity with O P; Cong.
Qed.


Lemma inc2_le_diam: forall O P A B U V, Diam A B O P -> InCircle U O P -> InCircle V O P -> Le U V A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Le Tn U V A B *)
unfold InCircle in *.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Le Tn U V A B *)
assert(HH:= segment_construction U O O V).
(* Goal: @Le Tn U V A B *)
ex_and HH W.
(* Goal: @Le Tn U V A B *)
assert(Le U V U W).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply (triangle_inequality U O); Between; Cong.
}

(* Goal: @Le Tn U V A B *)
assert(Le U W A B).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Le Tn U W A B *)
  apply(bet2_le2__le O O A B U W); Between.

(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply (l5_6 O U O P O U O A);Cong.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply (l5_6 O V O P O W O B);Cong.
}
(* Goal: @Le Tn U V A B *)
apply(le_transitivity U V U W A B); auto.
Qed.


Lemma onc_col_diam__eq : forall O P A B X, Diam A B O P -> OnCircle X O P -> Col A B X -> X = A \/ X = B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction(eq_dec_points O P).
(* Goal: False *)
treat_equalities.
(* Goal: or (@eq (@Tpoint Tn) T T) (@ReflectL Tn T T O A) *)
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
left; auto.

(* Goal: or (@eq (@Tpoint Tn) X A) (@eq (@Tpoint Tn) X B) *)
induction(eq_dec_points X B).
(* Goal: or (@Lt Tn T X T A) (@Cong Tn T A T X) *)
(* Goal: or (@Lt Tn T X T A) (@Cong Tn T A T X) *)
right; auto.
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
left.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
(* Goal: @eq (@Tpoint Tn) X A *)
assert(Cong O A O X) by (apply cong_transitivity with O P; Cong).
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
assert(Col A O X) by ColR.
(* Goal: @eq (@Tpoint Tn) X A *)
assert(HH:= l7_20 O A X H11 H10).
(* Goal: @OutCircleS Tn V O P *)
induction HH.
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
(* Goal: @eq (@Tpoint Tn) X A *)
assert(Midpoint O A B).
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
unfold Midpoint; split; trivial.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: False *)
apply H5.
(* Goal: @eq (@Tpoint Tn) O X *)
apply (symmetric_point_uniqueness A O ); auto.
Qed.

Lemma onc2_out__eq : forall O P A B, OnCircle A O P -> OnCircle B O P -> Out O A B -> A = B.
Proof.
(* Goal: forall (O P A B : @Tpoint Tn) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @Out Tn O A B), @eq (@Tpoint Tn) A B *)
  intros O P A B HAOn HBOn HOut.
(* Goal: @eq (@Tpoint Tn) A B *)
  destruct (symmetric_point_construction A O) as [A' HA'].
(* Goal: @eq (@Tpoint Tn) O X *)
  destruct (onc_col_diam__eq O P A A' B); auto.
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
    apply mid_onc__diam; assumption.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
    ColR.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X A B) (not (@OnCircle Tn X C D))) *)
  exfalso.
(* Goal: False *)
  subst A'.
(* Goal: False *)
  apply (not_bet_and_out A O B); Between.
Qed.

Lemma bet_onc_le_a : forall O P A B T X, Diam A B O P -> Bet B O T -> OnCircle X O P -> Le T A T X.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn B A O P *)
unfold Diam in*.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Le Tn T A T X *)
assert(Cong O X O A) by (apply cong_transitivity with O P; Cong).
(* Goal: @Le Tn T A T X *)
induction(eq_dec_points P O).
(* Goal: False *)
treat_equalities.
(* Goal: @Le Tn T P T P *)
(* Goal: @Le Tn T A T X *)
apply le_reflexivity.
(* Goal: @Le Tn T A T X *)
induction(eq_dec_points T O).
(* Goal: @Le Tn T A T X *)
(* Goal: @Le Tn T A T X *)
subst T.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong__le;Cong.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply(triangle_reverse_inequality O T X A); Cong.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
(* Goal: and (not (@eq (@Tpoint Tn) O T)) (and (not (@eq (@Tpoint Tn) A T)) (or (@Bet Tn T O A) (@Bet Tn T A O))) *)
repeat split; auto.
(* Goal: or (@Bet Tn O T A) (@Bet Tn O A T) *)
apply (l5_2 B); Between.
Qed.


Lemma bet_onc_lt_a : forall O P A B T X,
 Diam A B O P -> O <> P -> O <> T -> X <> A -> Bet B O T  -> OnCircle X O P ->
 Lt T A T X.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
assert(HH:= bet_onc_le_a O P A B T X H H3 H4).
assert(Lt T A T X \/ Cong T A T X).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: or (@Lt Tn T X T A) (@Cong Tn T A T X) *)
  induction(cong_dec T A T X).
(* Goal: or (@Lt Tn T X T A) (@Cong Tn T A T X) *)
(* Goal: or (@Lt Tn T X T A) (@Cong Tn T A T X) *)
  right; auto.
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
  left.
(* Goal: @Lt Tn T X T A *)
  unfold Lt.
(* Goal: and (@Midpoint Tn M X Y) (@Cong Tn A X A Y) *)
  split; auto.
}
(* Goal: @eq (@Tpoint Tn) O X *)
induction H5; auto.
(* Goal: @Diam Tn B A O P *)
unfold Diam in*.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
assert(Bet O A T \/ Bet O T A).
apply(l5_2 B O A T); Between.
(* Goal: @eq (@Tpoint Tn) X A *)
assert (Cong O A O X) by (apply cong_transitivity with O P; Cong).
induction H13.
assert(Bet O X T).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) O X *)
  apply(l4_6 O A T O X T); auto.
(* Goal: @Cong_3 Tn O A B O U V *)
  unfold Cong_3.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  repeat split; Cong.
}
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
apply H2.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply(between_cong_2 O T); Cong.
assert(Bet O T X).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) O X *)
  apply(l4_6 O T A O T X); auto.
(* Goal: @Cong_3 Tn O A B O U V *)
  unfold Cong_3.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  repeat split; Cong.
}
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
apply H2.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply(between_cong_3 O T); Cong.
Qed.



Lemma bet_onc_le_b : forall O P A B T X,
 Diam A B O P -> Bet A O T -> OnCircle X O P ->
 Le T X T A.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Le Tn T X T A *)
apply(triangle_inequality T O X A).
(* Goal: or (@Bet Tn T O A) (@Bet Tn T A O) *)
Between.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
Qed.


Lemma bet_onc_lt_b : forall O P A B T X,
 Diam A B O P -> T <> O -> X <> A -> Bet A O T -> OnCircle X O P ->
 Lt T X T A.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Lt Tn T X T A *)
assert(HH:= bet_onc_le_b O P A B T X H H2 H3 ).
assert(Lt T X  T A \/ Cong T A T X).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: or (@Lt Tn T X T A) (@Cong Tn T A T X) *)
  induction(cong_dec T A T X).
(* Goal: or (@Lt Tn T X T A) (@Cong Tn T A T X) *)
(* Goal: or (@Lt Tn T X T A) (@Cong Tn T A T X) *)
  right; auto.
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
  left.
(* Goal: @Lt Tn T X T A *)
  unfold Lt.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  split; Cong.
}
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @eq (@Tpoint Tn) O X *)
induction H4; auto.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: or (@Bet Tn T O A) (@Bet Tn T A O) *)
assert(Bet T O A) by eBetween.
(* Goal: False *)
assert(Bet T O X).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) O X *)
  apply(l4_6 T O A T O X); auto.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
  repeat split.
(* Goal: @Cong Tn T O T O *)
(* Goal: @Cong Tn T A T X *)
(* Goal: @Cong Tn O A O X *)
    apply cong_reflexivity.
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
    assumption.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
    apply cong_transitivity with O P; Cong.
}
(* Goal: False *)
apply H1.
(* Goal: @eq (@Tpoint Tn) X A *)
apply(between_cong_3 T O); trivial.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
Qed.



Lemma incs2_lt_diam : forall O P A B U V, Diam A B O P -> InCircleS U O P -> InCircleS V O P -> Lt U V A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
unfold Diam in H.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Lt Tn U V A B *)
unfold InCircleS in *.

(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction(eq_dec_points O P).
(* Goal: False *)
treat_equalities.
unfold Lt in H0.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
apply le_zero in H.
(* Goal: False *)
treat_equalities.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply H0; Cong.

assert(Lt A O A B /\ Lt B O A B).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) X A *)
  assert (Midpoint O A B).
    split; [assumption|apply cong_transitivity with O P; Cong].
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
  split.
(* Goal: not (@eq (@Tpoint Tn) M' U) *)
(* Goal: @Midpoint Tn M U V *)
  apply(mid__lt );  assert_diffs;auto.
  assert (Lt B O B A) by (apply mid__lt;assert_diffs;finish).
  auto using lt_right_comm.
}
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.

induction(eq_dec_points O U).
(* Goal: False *)
treat_equalities.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
assert(Lt O V O A).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(cong2_lt__lt O V O P); Cong.
}
(* Goal: @eq (@Tpoint Tn) O X *)
apply (lt_transitivity O V O A A B); auto.
(* Goal: @eq (@Tpoint Tn) O X *)
apply lt_left_comm; auto.

(* Goal: @Le Tn U V A B *)
assert(HH:=segment_construction U O O V).
ex_and HH V'.

assert(Le U V U V').
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(triangle_inequality U O V V' H8); Cong.
}
assert(Lt U V' A B).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply(bet2_lt2__lt O O A B U V' H8 H).
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(cong2_lt__lt O U O P O U O A); Cong.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(cong2_lt__lt O V O P O V' O B); Cong.
}

(* Goal: @eq (@Tpoint Tn) O X *)
apply(le1234_lt__lt U V U V' A B); auto.
Qed.

Lemma incs_onc_diam__lt : forall O P A B U V, Diam A B O P -> InCircleS U O P -> OnCircle V O P -> Lt U V A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Lt Tn U V A B *)
unfold InCircleS in *.

(* Goal: @Lt Tn U V A B *)
assert(HH:=segment_construction V O O U).
(* Goal: @Lt Tn U V A B *)
ex_and HH U'.
(* Goal: @Lt Tn U V A B *)
assert(Lt V U' A B).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Lt Tn V U' A B *)
  apply(bet2_lt_le__lt O O A B V U' H4 H).
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply cong_transitivity with O P; Cong.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(cong2_lt__lt O U O P); Cong.
}
(* Goal: @Lt Tn U V A B *)
assert(Le V U V U').
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(triangle_inequality V O U U' H4); Cong.
}
(* Goal: @Lt Tn U V A B *)
apply lt_left_comm.
(* Goal: @eq (@Tpoint Tn) O X *)
apply(le1234_lt__lt V U V U'); auto.
Qed.

Lemma diam_cong_incs__outcs : forall O P A B U V, Diam A B O P -> Cong A B U V -> InCircleS U O P -> OutCircleS V O P.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction(eq_dec_points O P).
(* Goal: False *)
treat_equalities.
(* Goal: @OutCircleS Tn V O O *)
(* Goal: @OutCircleS Tn V O P *)
unfold InCircleS in H1.

(* Goal: @OutCircleS Tn V O O *)
(* Goal: @OutCircleS Tn V O P *)
unfold Lt in H1.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @OutCircleS Tn V O O *)
(* Goal: @OutCircleS Tn V O P *)
apply le_zero in H1.
(* Goal: False *)
treat_equalities.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply H2; Cong.

(* Goal: @OutCircleS Tn V O P *)
assert(HH:= circle_cases O P V).
(* Goal: @OutCircleS Tn V O P *)
induction HH.
assert(Lt U V A B) by  apply(incs_onc_diam__lt O P A B U V H H1 H3).
(* Goal: @OutCircleS Tn V O P *)
(* Goal: @OutCircleS Tn V O P *)
unfold Lt in H4.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply H5; Cong.

(* Goal: @OutCircleS Tn V O P *)
induction H3.
(* Goal: @OutCircleS Tn V O P *)
(* Goal: @OutCircleS Tn V O P *)
assert(HH:=incs2_lt_diam O P A B U V H H1 H3).
(* Goal: @OutCircleS Tn V O P *)
(* Goal: @OutCircleS Tn V O P *)
unfold Lt in HH.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply H5; Cong.
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
assumption.
Qed.

Lemma diam_uniqueness : forall O P A B X, Diam A B O P -> Cong A X A B -> OnCircle X O P -> X = B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction(eq_dec_points O P).
(* Goal: @eq (@Tpoint Tn) O X *)
treat_equalities; auto.
(* Goal: @eq (@Tpoint Tn) X B *)
assert(Bet A O X).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) O X *)
  apply(l4_6 A O B A O X); auto.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  repeat split; Cong.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply cong_transitivity with O P; Cong.
}
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
(* Goal: @eq (@Tpoint Tn) O X *)
apply(between_cong_3 A O); auto.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
Qed.

Lemma onc3__ncol : forall O P A B C,
 A <> B -> A <> C -> B <> C ->
 OnCircle A O P -> OnCircle B O P -> OnCircle C O P ->
 ~ Col A B C.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
induction H5.
assert(InCircleS B O P).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply(bet_inc2__incs O P A C B); Circle.
}
(* Goal: @Lt Tn U V A B *)
unfold InCircleS in *.
unfold Lt in *.
(* Goal: @eq (@Tpoint Tn) O X *)
tauto.
induction H5.
assert(InCircleS C O P).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply(bet_inc2__incs O P B A C); Circle.
}
(* Goal: @Lt Tn U V A B *)
unfold InCircleS in *.
unfold Lt in *.
(* Goal: @eq (@Tpoint Tn) O X *)
tauto.
assert(InCircleS A O P).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply(bet_inc2__incs O P C B A); Circle.
}
(* Goal: @Lt Tn U V A B *)
unfold InCircleS in *.
unfold Lt in *.
(* Goal: @eq (@Tpoint Tn) O X *)
tauto.
Qed.

Lemma diam_exists : forall O P T, exists A, exists B, Diam A B O P /\ Col A B T.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Diam Tn A B O P) (@Col Tn A B T))) *)
destruct (diam_points O P T) as [A [B [HBet [HCol [HA HB]]]]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Diam Tn A B O P) (@Col Tn A B T))) *)
exists A, B.
(* Goal: and (not (@eq (@Tpoint Tn) O T)) (and (not (@eq (@Tpoint Tn) A T)) (or (@Bet Tn T O A) (@Bet Tn T A O))) *)
repeat split; auto.
Qed.

Lemma chord_intersection : forall O P A B X Y,
  OnCircle A O P -> OnCircle B O P -> OnCircle X O P -> OnCircle Y O P -> TS A B X Y ->
  TS X Y A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @TS Tn X Y A B *)
unfold TS in H3.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @TS Tn X Y A B *)
ex_and H5 T.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
repeat split.
(* Goal: not (@Col Tn B X Y) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T X Y) (@Bet Tn A T B)) *)
apply (onc3__ncol O P); Circle; try(intro; treat_equalities; Col).
(* Goal: not (@Col Tn B X Y) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T X Y) (@Bet Tn A T B)) *)
apply (onc3__ncol O P); Circle; try(intro; treat_equalities; Col).
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T X Y) (@Bet Tn A T B)) *)
exists T.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
Col.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply (col_inc_onc2__bet O P); Col.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(bet_inc2__incs O P X Y T); Circle; intro; treat_equalities; Col.
Qed.

Lemma ray_cut_chord : forall O P A B X Y,
  Diam A B O P -> OnCircle X O P -> OnCircle Y O P -> TS A B X Y -> OS X Y O A ->
  TS X Y O B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @TS Tn X Y O B *)
apply(l9_8_2 X Y A O B); [|Side].
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
apply (chord_intersection O P); assumption.
Qed.

Lemma center_col__diam : forall O P A B,
 A <> B -> Col O A B -> OnCircle A O P -> OnCircle B O P ->
 Diam A B O P.
Proof.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn A B O P *)
unfold Diam.
(* Goal: and (@Bet Tn A O B) (and (@OnCircle Tn A O P) (@OnCircle Tn B O P)) *)
split; Circle.
(* Goal: @Bet Tn A O B *)
assert(Cong O A O B) by (apply cong_transitivity with O P; Cong).
(* Goal: @Bet Tn A O B *)
assert(A = B \/ Midpoint O A B) by (apply(l7_20 O A B); Col).
(* Goal: @Bet Tn A O B *)
induction H4.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
contradiction.
(* Goal: or (@Bet Tn T O A) (@Bet Tn T A O) *)
Between.
Qed.

Lemma diam__midpoint: forall O P A B, Diam A B O P -> Midpoint O A B.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @Midpoint Tn O A B *)
unfold Midpoint.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
  assumption.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
Qed.

Lemma diam_sym : forall O P A B, Diam A B O P -> Diam B A O P.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: and (@Bet Tn B O A) (and (@OnCircle Tn B O P) (@OnCircle Tn A O P)) *)
repeat split; Between.
Qed.

Lemma diam_end_uniqueness : forall O P A B C, Diam A B O P -> Diam A C O P -> B = C.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @eq (@Tpoint Tn) B C *)
apply diam__midpoint in H.
(* Goal: @eq (@Tpoint Tn) B C *)
apply diam__midpoint in H0.
(* Goal: @eq (@Tpoint Tn) B C *)
apply (symmetric_point_uniqueness A O); Midpoint.
Qed.


Lemma center_onc2_mid__ncol : forall O P A B M ,
 O <> P -> ~ Col O A B ->
 OnCircle A O P -> OnCircle B O P ->
 Midpoint M A B  -> ~ Col A O M.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
unfold Midpoint in H3.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
apply H0.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
ColR.
Qed.

Lemma bet_chord__diam_or_ncol : forall O P A B T,
  A <> B -> T <> A -> T <> B -> OnCircle A O P -> OnCircle B O P -> Bet A T B ->
  Diam A B O P \/ ~Col O A T /\ ~Col O B T.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction(col_dec O A B).
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
left.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(center_col__diam); Col.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
right.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
apply H5; ColR.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
apply H5; ColR.
Qed.

Lemma mid_chord__diam_or_ncol : forall O P A B T,
 A <> B -> OnCircle A O P -> OnCircle B O P ->
 Midpoint T A B ->
 Diam A B O P \/ ~Col O A T /\ ~Col O B T.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@Diam Tn A B O P) (and (not (@Col Tn O A T)) (not (@Col Tn O B T))) *)
unfold Midpoint in H2.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @eq (@Tpoint Tn) O X *)
apply(bet_chord__diam_or_ncol);auto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: False *)
treat_equalities; tauto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: False *)
treat_equalities; tauto.
Qed.

Lemma cop_mid_onc2_perp__col : forall O P A B X Y, A <> B -> OnCircle A O P -> OnCircle B O P ->
  Midpoint X A B -> Perp X Y A B -> Coplanar O A B Y -> Col X Y O.
Proof.
(* Goal: forall (O P A B X Y : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @Midpoint Tn X A B) (_ : @Perp Tn X Y A B) (_ : @Coplanar Tn O A B Y), @Col Tn X Y O *)
  intros O P A B X Y HAB HAOn HBOn HX HPerp HCop.
(* Goal: @Col Tn X Y O *)
  destruct (eq_dec_points O X).
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    subst; Col.
(* Goal: @Col Tn X Y O *)
  apply cop_perp2__col with A B; Cop.
(* Goal: @eq (@Tpoint Tn) O X *)
  apply perp_left_comm, mid_onc2__perp with P; auto.
Qed.

Lemma cong2_cop2_onc3__eq : forall O P X A B C, A <> B -> A <> C -> B <> C ->
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O ->
  Cong X A X B -> Cong X A X C -> Coplanar A B C X ->
  X = O.
Proof.
(* Goal: forall (O P X A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @Coplanar Tn A B C O) (_ : @Cong Tn X A X B) (_ : @Cong Tn X A X C) (_ : @Coplanar Tn A B C X), @eq (@Tpoint Tn) X O *)
  intros O P X A B C HAB HAC HBC HAOn HBOn HCOn HCop HCong1 HCong2 HCop1.
(* Goal: @eq (@Tpoint Tn) X O *)
  destruct (midpoint_existence A B) as [M1 HM1].
(* Goal: @eq (@Tpoint Tn) X O *)
  destruct (midpoint_existence A C) as [M2 HM2].
(* Goal: @eq (@Tpoint Tn) X O *)
  assert (HNCol : ~ Col C A B) by (apply (onc3__ncol O P); auto).
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  destruct (l10_15 A B M1 C) as [P1 [HPerp1 HOS1]]; Col.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  destruct (l10_15 A C M2 B) as [P2 [HPerp2 HOS2]]; Col.
(* Goal: @eq (@Tpoint Tn) X O *)
  assert (HColX1 : Col M1 P1 X).
(* Goal: @Col Tn M1 P1 X *)
(* Goal: @eq (@Tpoint Tn) X O *)
    apply (cop_mid_onc2_perp__col X A A B); Circle; Perp.
(* Goal: @Coplanar Tn O A B P1 *)
(* Goal: @eq (@Tpoint Tn) X O *)
    apply coplanar_perm_12, coplanar_trans_1 with C; Cop.
(* Goal: @eq (@Tpoint Tn) X O *)
  assert (HColO1 : Col M1 P1 O).
(* Goal: @Col Tn M1 P1 O *)
(* Goal: @eq (@Tpoint Tn) X O *)
    apply (cop_mid_onc2_perp__col O P A B); Perp.
(* Goal: @Coplanar Tn O A B P1 *)
(* Goal: @eq (@Tpoint Tn) X O *)
    apply coplanar_perm_12, coplanar_trans_1 with C; Cop.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  apply not_col_permutation_3 in HNCol.
(* Goal: @eq (@Tpoint Tn) X O *)
  assert (HColX2 : Col M2 P2 X).
(* Goal: @Col Tn M2 P2 X *)
(* Goal: @eq (@Tpoint Tn) X O *)
    apply (cop_mid_onc2_perp__col X A A C); Circle; Perp.
(* Goal: @Coplanar Tn O A C P2 *)
(* Goal: @eq (@Tpoint Tn) X O *)
    apply coplanar_perm_12, coplanar_trans_1 with B; Cop.
(* Goal: @eq (@Tpoint Tn) X O *)
  assert (HColO2 : Col M2 P2 O).
(* Goal: @Col Tn M2 P2 O *)
(* Goal: @eq (@Tpoint Tn) X O *)
    apply (cop_mid_onc2_perp__col O P A C); Perp.
(* Goal: @Coplanar Tn O A C P2 *)
(* Goal: @eq (@Tpoint Tn) X O *)
    apply coplanar_perm_12, coplanar_trans_1 with B; Cop.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
  assert_diffs.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  destruct (col_dec M1 P1 M2); [apply (l6_21 M2 P2 M1 P1)|apply (l6_21 M1 P1 M2 P2)]; Col.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  apply HBC.
(* Goal: @eq (@Tpoint Tn) B C *)
  destruct (eq_dec_points M1 M2).
(* Goal: @eq (@Tpoint Tn) B C *)
(* Goal: @eq (@Tpoint Tn) B C *)
    apply (symmetric_point_uniqueness A M1); subst; trivial.
(* Goal: @eq (@Tpoint Tn) B C *)
  apply l10_2_uniqueness_spec with M1 P1 A.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    split; Perp; exists M1; Col.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
  split.
(* Goal: @eq (@Tpoint Tn) O X *)
    exists M2; auto.
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
  left.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
  apply perp_sym, perp_col2_bis with P2 M2; ColR.
Qed.

Lemma tree_points_onc_cop : forall O P, O <> P -> exists A B C,
  A <> B /\ A <> C /\ B <> C /\ OnCircle A O P /\ OnCircle B O P /\ OnCircle C O P /\ Coplanar A B C O.
Proof.
(* Goal: forall (O P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) O P)), @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (@OnCircle Tn C O P)))))))) *)
  intros O P HOP.
(* Goal: @eq (@Tpoint Tn) O X *)
  destruct (not_col_exists O P) as [X HNCol]; auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
  destruct (diam_points O P X) as [B [C [HBet [HCol []]]]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (@Coplanar Tn A B C O))))))))) *)
  exists P, B, C.
(* Goal: and (@Bet Tn A O B) (and (@OnCircle Tn A O P) (@OnCircle Tn B O P)) *)
  repeat split; Circle.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
    intro; subst; apply HNCol; ColR.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
    intro; subst; apply HNCol; ColR.
(* Goal: not (@eq (@Tpoint Tn) C1 O) *)
(* Goal: not (@eq (@Tpoint Tn) C1 I) *)
    intro; treat_equalities; auto.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    exists B; left; split; Col.
Qed.

Lemma tree_points_onc_cop2 : forall O P Q, O <> P -> exists A B C,
  A <> B /\ A <> C /\ B <> C /\ OnCircle A O P /\ OnCircle B O P /\ OnCircle C O P /\
  Coplanar A B C O /\ Coplanar A B C Q.
Proof.
(* Goal: forall (O P Q : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) O P)), @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
  intros O P Q HOP.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
  destruct (eq_dec_points O Q).
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
    subst Q.
(* Goal: @eq (@Tpoint Tn) O X *)
    destruct (tree_points_onc_cop O P HOP) as [A [B [C]]]; spliter.
(* Goal: and (not (@eq (@Tpoint Tn) O T)) (and (not (@eq (@Tpoint Tn) A T)) (or (@Bet Tn T O A) (@Bet Tn T A O))) *)
    exists A, B, C; repeat split; auto.
(* Goal: @eq (@Tpoint Tn) O X *)
  destruct (not_col_exists O Q) as [X HNCol]; auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
  destruct (diam_points O P X) as [B [C [HBet [HCol []]]]].
(* Goal: @eq (@Tpoint Tn) O X *)
  destruct (l6_11_existence O O P Q) as [A []]; auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q)))))))))) *)
  exists A, B, C.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (and (@OnCircle Tn C O P) (and (@Coplanar Tn A B C O) (@Coplanar Tn A B C Q))))))) *)
  assert (~ Col O A B) by (intro; unfold OnCircle in *; assert_diffs; apply HNCol; ColR).
(* Goal: not (@eq (@Tpoint Tn) M U) *)
  assert_diffs.
(* Goal: and (@Bet Tn A O B) (and (@OnCircle Tn A O P) (@OnCircle Tn B O P)) *)
  repeat split; Circle.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
    intro; subst; apply HNCol; ColR.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    exists B; left; split; Col.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
    exists O; right; right; split; Col.
Qed.

Lemma tree_points_onc : forall O P, O <> P -> exists A B C,
  A <> B /\ A <> C /\ B <> C /\ OnCircle A O P /\ OnCircle B O P /\ OnCircle C O P.
Proof.
(* Goal: forall (O P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) O P)), @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) B C)) (and (@OnCircle Tn A O P) (and (@OnCircle Tn B O P) (@OnCircle Tn C O P)))))))) *)
  intros O P HOP.
(* Goal: @eq (@Tpoint Tn) O X *)
  destruct (tree_points_onc_cop O P HOP) as [A [B [C]]]; spliter.
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
  exists A, B, C; repeat split; assumption.
Qed.

Lemma bet_cop_onc2__ex_onc_os_out : forall O P A B C I,
  A <> I -> B <> I -> ~ Col A B C -> ~ Col A B O ->
  OnCircle A O P -> OnCircle B O P -> Bet A I B -> Coplanar A B C O ->
  exists C1, Out C1 O I /\ OnCircle C1 O P /\ OS A B C C1.
Proof.
(* Goal: forall (O P A B C I : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A I)) (_ : not (@eq (@Tpoint Tn) B I)) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B O)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @Bet Tn A I B) (_ : @Coplanar Tn A B C O), @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => and (@Out Tn C1 O I) (and (@OnCircle Tn C1 O P) (@OS Tn A B C C1))) *)
  intros O P A B C I HAI HBI HNCol HNCol1 HA HB HBet HCop.
(* Goal: @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => and (@Out Tn C1 O I) (and (@OnCircle Tn C1 O P) (@OS Tn A B C C1))) *)
  destruct (diam_points O P I) as [C1 [C2 [HBet1 [HCol [HC1 HC2]]]]].
(* Goal: @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => and (@Out Tn C1 O I) (and (@OnCircle Tn C1 O P) (@OS Tn A B C C1))) *)
  assert (HTS : TS A B C1 C2).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
  { apply (chord_intersection O P); trivial.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
    unfold OnCircle in *; assert_diffs.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
    repeat split; [intro; apply HNCol1; ColR..|exists I; split; Col].
  }
(* Goal: @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => and (@Out Tn C1 O I) (and (@OnCircle Tn C1 O P) (@OS Tn A B C C1))) *)
  assert (HBet2 : Bet C1 I C2).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
  { assert_diffs; apply (col_inc_onc2__bet O P); auto.
(* Goal: @InCircle Tn I O P *)
    apply bet_inc2__inc with A B; Circle.
  }
(* Goal: @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => and (@Out Tn C1 O I) (and (@OnCircle Tn C1 O P) (@OS Tn A B C C1))) *)
  assert (HNCol2 : ~ Col C1 A B) by (destruct HTS; assumption).
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  destruct (cop__one_or_two_sides A B C C1); Col.
(* Goal: @Coplanar Tn A B C C1 *)
(* Goal: @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => and (@Out Tn C1 O I) (and (@OnCircle Tn C1 O P) (@OS Tn A B C C1))) *)
(* Goal: @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => and (@Out Tn C1 O I) (and (@OnCircle Tn C1 O P) (@OS Tn A B C C1))) *)
    apply coplanar_trans_1 with O; Col; [Cop|exists I; right; right; assert_diffs; split; ColR].
  - exists C2.
(* Goal: and (@Out Tn C2 O I) (and (@OnCircle Tn C2 O P) (@OS Tn A B C C2)) *)
    split; [|split; trivial; exists C1; Side].
(* Goal: or (@Bet Tn T O A) (@Bet Tn T A O) *)
    apply bet2__out with C1; Between.
(* Goal: not (@eq (@Tpoint Tn) C1 O) *)
(* Goal: not (@eq (@Tpoint Tn) C1 I) *)
      intro; treat_equalities; auto.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
      destruct HTS as [_ [HNCol3 _]]; spliter; intro; subst; apply HNCol3; Col.
  - exists C1.
(* Goal: and (@Out Tn C1 O I) (and (@OnCircle Tn C1 O P) (@OS Tn A B C C1)) *)
    split; [|split; trivial].
(* Goal: @Out Tn C1 O I *)
    apply bet2__out with C2; trivial.
(* Goal: not (@eq (@Tpoint Tn) C1 O) *)
(* Goal: not (@eq (@Tpoint Tn) C1 I) *)
      intro; treat_equalities; auto.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
      intro; subst; apply HNCol2; Col.
Qed.

(** Two circles are equal if and only if they have the same center and the same radius *)

Lemma EqC_chara: forall A B C D, EqC A B C D <-> A = C /\ Cong A B C D.
Proof.
(* Goal: forall A B C D : @Tpoint Tn, iff (@EqC Tn A B C D) (and (@eq (@Tpoint Tn) A C) (@Cong Tn A B C D)) *)
  intros A B C D.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
  split.
  - intro Heq.
(* Goal: and (@eq (@Tpoint Tn) A C) (@Cong Tn A B C D) *)
    unfold EqC in Heq.
(* Goal: and (@eq (@Tpoint Tn) A C) (@Cong Tn A B C D) *)
    assert (C = A).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
    { destruct (eq_dec_points A B) as [|Hd].
      - subst B.
(* Goal: @Cong Tn A B A D *)
        unfold OnCircle in Heq.
(* Goal: @eq (@Tpoint Tn) C A *)
        assert (Cong A D A A) by (rewrite Heq; Cong).
(* Goal: False *)
        treat_equalities.
(* Goal: @eq (@Tpoint Tn) C A *)
        destruct (segment_construction A C A C) as [A' []].
(* Goal: @eq (@Tpoint Tn) C A *)
        assert (Cong A A' A A) by (rewrite Heq; Cong).
(* Goal: @eq (@Tpoint Tn) O X *)
        treat_equalities; auto.
      - destruct (tree_points_onc_cop2 A B C Hd) as [B0 [B1 [B2]]].
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
        spliter; unfold OnCircle in *.
        assert (Cong C B0 C D) by (rewrite <- Heq; Cong).
        apply cong2_cop2_onc3__eq with B B0 B1 B2; auto;
          apply cong_transitivity with C D; trivial;
          unfold OnCircle in *; apply cong_symmetry; rewrite <- Heq; assumption.
    }
(* Goal: @EqC Tn A B C D *)
    subst C.
(* Goal: and (@eq (@Tpoint Tn) A A) (@Cong Tn A B A D) *)
    split; trivial.
(* Goal: @Cong Tn A B A D *)
    unfold OnCircle in Heq.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
    rewrite <- (Heq B); Cong.
  - intros [].
(* Goal: @EqC Tn A B C D *)
    subst C.
(* Goal: @EqC Tn A B A D *)
    intro X.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
    split; intro; [apply cong_transitivity with A B|apply cong_transitivity with A D]; Cong.
Qed.

(** Two circles are distinct if and only if there is a point
    belonging to the first and not to the second *)

Lemma nEqC_chara : forall A B C D, A <> B ->
  ~ EqC A B C D <->
  (exists X, OnCircle X A B /\ ~ OnCircle X C D).
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)), iff (not (@EqC Tn A B C D)) (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X A B) (not (@OnCircle Tn X C D)))) *)
  intros A B C D HAB.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
  split.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
  { intro Hneq.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X A B) (not (@OnCircle Tn X C D))) *)
    destruct (eq_dec_points C A) as [|HCA].
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
    { destruct (cong_dec A B C D) as [|HNCong].
(* Goal: and (@Midpoint Tn M X Y) (@Cong Tn A X A Y) *)
        exfalso; apply Hneq, EqC_chara; split; auto.
(* Goal: and (@Bet Tn A O B) (and (@OnCircle Tn A O P) (@OnCircle Tn B O P)) *)
        subst C; exists B; split; Circle.
    }
(* Goal: @eq (@Tpoint Tn) O X *)
    destruct (tree_points_onc_cop2 A B C HAB) as [B0 [B1 [B2]]]; spliter.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X A B) (not (@OnCircle Tn X C D))) *)
    destruct (cong_dec C B0 C D); [destruct (cong_dec C B1 C D);[destruct (cong_dec C B2 C D)|]|].
    - exfalso.
(* Goal: False *)
      apply HCA.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
      apply cong2_cop2_onc3__eq with B B0 B1 B2; auto; apply cong_transitivity with C D; Cong.
    - exists B2; auto.
    - exists B1; auto.
    - exists B0; auto.
  }
(* Goal: forall _ : @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@OnCircle Tn X A B) (not (@OnCircle Tn X C D))), not (@EqC Tn A B C D) *)
  intros [X [HX Habs]] Heq.
(* Goal: False *)
  apply Habs, Heq, HX.
Qed.

Lemma EqC_sym : forall A B C D, EqC A B C D -> EqC C D A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @EqC Tn A B C D), @EqC Tn C D A B *)
  intros A B C D Heq X.
  split; intro; [rewrite (Heq X)|rewrite <- (Heq X)]; assumption.
Qed.

End Circle_2.

Section Circle_2D.

(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
Context `{T2D:Tarski_2D}.

(** The center of a circle belongs to the perpendicular bisector of each chord *)

Lemma mid_onc2_perp__col : forall O P A B X Y,
 A <> B -> OnCircle A O P -> OnCircle B O P -> Midpoint X A B -> Perp X Y A B -> Col X Y O.
Proof.
(* Goal: forall (O P A B X Y : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @Midpoint Tn X A B) (_ : @Perp Tn X Y A B), @Col Tn X Y O *)
  intros O P A B X Y HAB HAOn HBOn HX HPerp.
(* Goal: @Col Tn X Y O *)
  assert (HCop := all_coplanar O A B Y).
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
  apply cop_mid_onc2_perp__col with P A B; assumption.
Qed.

(** Euclid Book III Prop 4.
 If in a circle two straight lines which do not pass through the center cut one another,
 then they do not bisect one another.
 *)

Lemma mid2_onc4__eq : forall O P A B C D X, B <> C-> A <> B -> 
 OnCircle A O P ->
 OnCircle B O P ->
 OnCircle C O P ->
 OnCircle D O P ->
 Midpoint X A C ->
 Midpoint X B D ->
 X=O.
Proof.
intros O P A B C D X Hbc.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
assert(HH:=mid_onc2__per O P A C X H0 H2 H4).
assert(HP:=mid_onc2__per O P B D X H1 H3 H5).

induction(eq_dec_points X O).
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
assert(Col A B X).
apply(per2__col A B O X); Perp.
(* Goal: @Perp Tn O A Y X *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
assert(Col B X D).
(* Goal: @eq (@Tpoint Tn) O X *)
apply bet_col; auto.
assert(Col A X C).
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
ColR.

induction(eq_dec_points A X).
(* Goal: @eq (@Tpoint Tn) O X *)
(* Goal: @eq (@Tpoint Tn) O X *)
subst X.
(* Goal: False *)
treat_equalities.
assert(OutCircleS D O P).
(* Goal: @eq (@Tpoint Tn) O X *)
apply(onc2_out__outcs O P A B D); auto.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
(* Goal: @Out Tn T O A *)
unfold Out.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
(* Goal: or (@Bet Tn T O A) (@Bet Tn T A O) *)
left; Between.

unfold OutCircleS in *.
unfold Lt in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
unfold OnCircle in H3.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
absurd (Cong O P O D);Cong.

assert(Col A B C). 
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
ColR.

assert(C = A \/ C = B).
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(line_circle_two_points O P A B C); Col.
destruct H14.
(* Goal: False *)
treat_equalities.
(* Goal: False *)
intuition.
(* Goal: False *)
treat_equalities.
assert(A = D) by
(apply (symmetric_point_uniqueness C X); split; Between; Cong).
(* Goal: False *)
treat_equalities.
(* Goal: @eq (@Tpoint Tn) O X *)
tauto.
Qed.

(** Euclid Book III Prop 9.
 If a point is taken within a circle,
 and more than two equal straight lines fall from the point on the circle,
 then the point taken is the center of the circle.
*)

Lemma cong2_onc3__eq : forall O P X A B C, A <> B -> A <> C -> B <> C ->
  OnCircle A O P -> OnCircle B O P -> OnCircle C O P ->
  Cong X A X B -> Cong X A X C ->
  X = O.
Proof.
(* Goal: forall (O P X A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @Cong Tn X A X B) (_ : @Cong Tn X A X C), @eq (@Tpoint Tn) X O *)
  intros O P X A B C HAB HAC HBC HAOn HBOn HCOn HCong1 HCong2.
(* Goal: @eq (@Tpoint Tn) X O *)
  assert (HCop := all_coplanar A B C O).
(* Goal: @eq (@Tpoint Tn) X O *)
  assert (HCop1 := all_coplanar A B C X).
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
  apply cong2_cop2_onc3__eq with P A B C; assumption.
Qed.

Lemma onc2_mid_cong_col : forall O P U V M X,
 U <> V ->OnCircle U O P -> OnCircle V O P -> Midpoint M U V -> Cong U X V X -> Col O X M.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Col Tn O X M *)
assert(HH:=mid_onc2__per O P U V M H0 H1 H2).
(* Goal: @Col Tn O X M *)
assert(Per X M U).
(* Goal: @Per Tn A M X *)
unfold Per.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn M U C') (@Cong Tn X U X C')) *)
(* Goal: @Col Tn O X M *)
exists V.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
split; Cong.
(* Goal: @eq (@Tpoint Tn) O X *)
apply(per2__col _ _ U); auto.
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
Qed.


Lemma cong_onc3_cases : forall O P A X Y,
 Cong A X A Y ->
 OnCircle A O P -> OnCircle X O P -> OnCircle Y O P ->
 X = Y \/ ReflectL X Y O A.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
induction(eq_dec_points X Y).
(* Goal: or (@eq (@Tpoint Tn) T T) (@ReflectL Tn T T O A) *)
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
left; auto.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
right.
(* Goal: @ReflectL Tn X Y O A *)
assert(HH:= midpoint_existence X Y).
(* Goal: @eq (@Tpoint Tn) O X *)
ex_and HH M.
(* Goal: @ReflectL Tn X Y O A *)
assert(Per O M X).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Per Tn O M X *)
  apply(mid_onc2__per O P X Y M); Circle.
}
(* Goal: @ReflectL Tn X Y O A *)
assert(Per A M X).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Per Tn A M X *)
  unfold Per.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn M X C') (@Cong Tn A X A C')) *)
  exists Y.
(* Goal: and (@Midpoint Tn M X Y) (@Cong Tn A X A Y) *)
  split; auto.
}
(* Goal: @ReflectL Tn X Y O A *)
assert(Col A O M).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) O X *)
  apply (per2__col _ _ X); auto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  treat_equalities; tauto.
}

(* Goal: @ReflectL Tn X Y O A *)
unfold ReflectL.
(* Goal: and (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0))) (or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X)) *)
split.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn O A X0)) *)
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
exists M.
(* Goal: and (@Midpoint Tn M Y X) (@Col Tn O A M) *)
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
split; Midpoint.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
Col.
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
left.

(* Goal: @Perp Tn O A Y X *)
unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.

(* Goal: @Perp Tn O A Y X *)
induction(eq_dec_points M O).
(* Goal: @Perp Tn O A Y X *)
(* Goal: @Perp Tn O A Y X *)
subst M.
(* Goal: @Perp Tn O A Y X *)
(* Goal: @Perp Tn O A Y X *)
apply per_perp_in in H6.
(* Goal: @Perp Tn O A Y X *)
(* Goal: not (@eq (@Tpoint Tn) A O) *)
(* Goal: not (@eq (@Tpoint Tn) O X) *)
(* Goal: @Perp Tn O A Y X *)
apply perp_in_comm in H6.
(* Goal: @Perp Tn O A Y X *)
(* Goal: not (@eq (@Tpoint Tn) A O) *)
(* Goal: not (@eq (@Tpoint Tn) O X) *)
(* Goal: @Perp Tn O A Y X *)
apply perp_in_perp in H6.
(* Goal: @Perp Tn O A Y X *)
(* Goal: not (@eq (@Tpoint Tn) A O) *)
(* Goal: not (@eq (@Tpoint Tn) O X) *)
(* Goal: @Perp Tn O A Y X *)
apply perp_sym in H6.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply (perp_col X O O A Y) in H6; Col.
(* Goal: @Perp Tn O M Y X *)
(* Goal: @Col Tn X M Y *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
Perp.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: False *)
treat_equalities; tauto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: False *)
treat_equalities; tauto.

(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(perp_col O M Y X A);Col.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: False *)
treat_equalities; tauto.
(* Goal: @Perp Tn O M Y X *)
apply per_perp_in in H5.
(* Goal: @Perp Tn O M Y X *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
apply perp_in_comm in H5.
(* Goal: @Perp Tn O M Y X *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
apply perp_in_perp in H5.
(* Goal: @Perp Tn O M Y X *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
apply perp_sym in H5.
(* Goal: @eq (@Tpoint Tn) O X *)
apply(perp_col X M M O Y) in H5; auto.
(* Goal: @Perp Tn O M Y X *)
(* Goal: @Col Tn X M Y *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
Perp.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
Col.
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: False *)
treat_equalities; tauto.
Qed.


Lemma bet_cong_onc3_cases : forall O P A X Y T,
 T <> O -> Bet A O T -> Cong T X T Y ->
 OnCircle A O P  -> OnCircle X O P  -> OnCircle Y O P ->
 X = Y \/ ReflectL X Y O A.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction(eq_dec_points O P).
(* Goal: False *)
treat_equalities.
(* Goal: or (@eq (@Tpoint Tn) T T) (@ReflectL Tn T T O A) *)
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
left; auto.

(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
induction(eq_dec_points T X).
(* Goal: False *)
treat_equalities.
(* Goal: or (@eq (@Tpoint Tn) T T) (@ReflectL Tn T T O A) *)
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
left; auto.

(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
assert(CongA T O X T O Y /\ CongA O T X O T Y /\ CongA T X O T Y O).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(l11_51 O T X O T Y); Cong.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
    intro.
(* Goal: False *)
    treat_equalities; tauto.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply cong_transitivity with O P; Cong.
}
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
assert(Out T O A).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Out Tn T O A *)
  unfold Out.
(* Goal: and (not (@eq (@Tpoint Tn) O T)) (and (not (@eq (@Tpoint Tn) A T)) (or (@Bet Tn T O A) (@Bet Tn T A O))) *)
  repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  treat_equalities; tauto.
(* Goal: or (@Bet Tn T O A) (@Bet Tn T A O) *)
  Between.
}
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
assert(Cong A X A Y).
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
{ apply(cong2_conga_cong A T X A T Y); Cong.
(* Goal: @eq (@Tpoint Tn) O X *)
  apply (out_conga O T X O T Y); auto.
(* Goal: @eq (@Tpoint Tn) O X *)
  apply out_trivial; auto.
(* Goal: @Out Tn T Y Y *)
  apply out_trivial.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  treat_equalities; tauto.
}
(* Goal: @eq (@Tpoint Tn) O X *)
apply (cong_onc3_cases O P); auto.
Qed.

Lemma prop_7_8 : forall O P A B T X Y , Diam A B O P -> Bet A O T 
                               -> OnCircle X O P -> OnCircle Y O P
                               -> LeA A O X A O Y -> Le T Y T X.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
assert(HD:=H).
unfold Diam in H.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction(eq_dec_points O P).
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q2 : @Tpoint Tn => and (@Bet Tn Q1 O Q2) (and (@Col Tn Q1 Q2 X) (and (@OnCircle Tn Q1 O P) (@OnCircle Tn Q2 O P))))) *)
subst P.
(* Goal: @eq (@Tpoint Tn) O X *)
treat_equalities; auto.
(* Goal: @Le Tn T P T P *)
(* Goal: @Le Tn T A T X *)
apply le_reflexivity.

induction(eq_dec_points O T).
(* Goal: False *)
treat_equalities.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong__le, cong_transitivity with O P; Cong.

induction(cong_dec A X A Y).
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
assert(X = Y \/ ReflectL X Y O A).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply(cong_onc3_cases O P A X Y); Circle.
}
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction H9.
(* Goal: False *)
treat_equalities.
(* Goal: @Le Tn T P T P *)
(* Goal: @Le Tn T A T X *)
apply le_reflexivity.
apply cong__le.
(* Goal: @Cong Tn N O M O *)
apply cong_symmetry.
(* Goal: @Cong Tn O N O M *)
apply cong_commutativity.
(* Goal: @eq (@Tpoint Tn) O X *)
apply(is_image_spec_col_cong O A X Y T); auto.
(* Goal: @Diam Tn B A O P *)
unfold Diam in *.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @Col Tn A A' B *)
(* Goal: @eq (@Tpoint Tn) A B *)
ColR.

assert(Le T X T A).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply(bet_onc_le_b O P A B T X HD H0).
  Circle.
}
(* Goal: not (@eq (@Tpoint Tn) M U) *)
assert_diffs.

assert(LeA Y O T X O T).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply lea_comm.
(* Goal: @eq (@Tpoint Tn) O X *)
  apply(l11_36 A O X A O Y T T); auto.
}

assert(Lt T Y T X).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  assert(Cong O X O Y) by (apply cong_transitivity with O P; Cong).
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(t18_18 O T X O T Y); Cong.
  unfold LtA.
(* Goal: and (@Midpoint Tn M X Y) (@Cong Tn A X A Y) *)
  split; auto.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
  assert(Cong Y T X T).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
  {
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
    apply(cong2_conga_cong Y O T X O T); Cong.
  }
  assert(CongA A O X A O Y).
(* Goal: or (@Bet Tn T O A) (@Bet Tn T A O) *)
  apply(l11_13 T O X T O Y A A); Between.
  CongA.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  apply H8.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply(cong2_conga_cong A O X A O Y); Cong.
}
apply lt__le.
(* Goal: @Bet Tn A O B *)
(* Goal: @Cong Tn A O O B *)
assumption.
Qed.




Lemma Prop_7_8_uniqueness : forall O P A X Y Z T, T <> O -> X <> Y ->
  Bet A O T -> Cong T X T Y -> Cong T X T Z ->
  OnCircle A O P -> OnCircle X O P -> OnCircle Y O P -> OnCircle Z O P ->
  Z = X \/ Z = Y.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction(eq_dec_points O P).
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: False *)
treat_equalities.
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
assert(X = Y \/ ReflectL X Y O A).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) O X *)
  apply(bet_cong_onc3_cases O P A X Y T); auto.
}
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
assert(X = Z \/ ReflectL X Z O A).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) O X *)
  apply(bet_cong_onc3_cases O P A X Z T); auto.
}
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
assert(Y = Z \/ ReflectL Y Z O A).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @eq (@Tpoint Tn) O X *)
  apply(bet_cong_onc3_cases O P A Y Z T); auto.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply cong_transitivity with T X; Cong.
}
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction H9.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
contradiction.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction H10.
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
induction H11.
(* Goal: @eq (@Tpoint Tn) O X *)
auto.
(* Goal: or (@eq (@Tpoint Tn) Z X) (@eq (@Tpoint Tn) Z Y) *)
assert(HH:=l10_2_uniqueness_spec O A Z X Y H10 H11).
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
contradiction.
Qed.

Lemma chords_midpoints_col_par : forall O P A M B C N D, 
 O <> P ->
 OnCircle A O P -> OnCircle B O P ->
 OnCircle C O P -> OnCircle D O P ->
 Midpoint M A B -> Midpoint N C D ->
 Col O M N -> ~ Col O A B -> ~ Col O C D -> Par A B C D.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
(* Goal: @Par Tn A B C D *)
assert(Perp O M A B).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply(mid_onc2__perp O  P A B M); Circle.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  treat_equalities.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
  apply H7.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  Col.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  treat_equalities.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  apply H7; Col.
}
(* Goal: @Par Tn A B C D *)
assert(Perp O N C D).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
  apply(mid_onc2__perp O  P C D N); Circle.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  treat_equalities.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  apply H8.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  Col.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  treat_equalities.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  apply H8; Col.
}
(* Goal: @Par Tn A B C D *)
assert(Perp O M C D).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  apply (perp_col O N C D M); Col.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
  intro.
(* Goal: False *)
  treat_equalities.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  apply H7; Col.
}
(* Goal: @Perp Tn O M Y X *)
(* Goal: @Col Tn X M Y *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
apply (l12_9_2D A B C D O M); Perp.
Qed.

Lemma onc3_mid2__ncol : forall O P A B C A' B',
 O <> P -> 
 OnCircle A O P -> OnCircle B O P -> OnCircle C O P ->
 Midpoint A' A C -> Midpoint B' B C -> ~ Col A B C ->
 ~ Col O A' B' \/ A' = O \/ B' = O.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.
induction(col_dec O A C).
assert(A = C \/ Midpoint O A C).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
  unfold OnCircle in *.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply l7_20; eCong.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  Col.
}
induction H7.
(* Goal: False *)
treat_equalities.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply H5; Col.
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
right; left.
(* Goal: @eq (@Tpoint Tn) O X *)
apply (l7_17 A C); auto.

induction(col_dec O B C).
assert(B = C \/ Midpoint O B C).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
  unfold OnCircle in *.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
  apply l7_20; eCong.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
  Col.
}
induction H8.
(* Goal: False *)
treat_equalities.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply H5; Col.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y O A) *)
right; right.
(* Goal: @eq (@Tpoint Tn) O X *)
apply (l7_17 B C); auto.
(* Goal: or (@Perp Tn O A Y X) (@eq (@Tpoint Tn) Y X) *)
left.
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
assert(HH:=chords_midpoints_col_par O P A A' C B B' C H H0 H2 H1 H2 H3 H4 H8 H6 H7).
(* Goal: @OutCircleS Tn V O P *)
induction HH.
apply H9.
exists C.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
split; Col.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
spliter; contradiction.
Qed.

(** Euclid Book III Prop 9.
 If a point is taken within a circle,
 and more than two equal straight lines fall from the point on the circle, 
 then the point taken is the center of the circle.*)

Lemma onc4_cong2__eq: 
 forall A B C D O P X,
 A<>B -> C<>D ->
 ~ Par A B C D ->
 OnCircle A O P ->
 OnCircle B O P ->
 OnCircle C O P ->
 OnCircle D O P ->
 Cong A X B X ->
 Cong C X D X ->
 O=X.
Proof.
(* Goal: forall (A B C D O P X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@Par Tn A B C D)) (_ : @OnCircle Tn A O P) (_ : @OnCircle Tn B O P) (_ : @OnCircle Tn C O P) (_ : @OnCircle Tn D O P) (_ : @Cong Tn A X B X) (_ : @Cong Tn C X D X), @eq (@Tpoint Tn) O X *)
intros.

(* Goal: @eq (@Tpoint Tn) O X *)
assert(HP:O <> P).
(* Goal: not (@eq (@Tpoint Tn) O P) *)
(* Goal: @eq (@Tpoint Tn) O X *)
{
(* Goal: not (@eq (@Tpoint Tn) O P) *)
intro.
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: False *)
treat_equalities. intuition.
}

(* Goal: @eq (@Tpoint Tn) O X *)
assert(HH:= midpoint_existence A B).
(* Goal: @eq (@Tpoint Tn) O X *)
ex_and HH M.
(* Goal: @eq (@Tpoint Tn) O X *)
assert(HH:= midpoint_existence C D).
(* Goal: @eq (@Tpoint Tn) O X *)
ex_and HH N.

assert(Col O X M)
 by (apply(onc2_mid_cong_col O P A B M X); auto).
assert(Col O X N)
 by (apply(onc2_mid_cong_col O P C D N X); auto).

(* Goal: @eq (@Tpoint Tn) O X *)
induction(eq_dec_points O X).
- auto.
- assert(Col O M N); eCol.


(* Goal: @eq (@Tpoint Tn) O X *)
assert(HH1:=cong_perp_or_mid A B M X H H8 H6).
(* Goal: @eq (@Tpoint Tn) O X *)
assert(HH2:=cong_perp_or_mid C D N X H0 H9 H7).

(* Goal: @eq (@Tpoint Tn) O X *)
induction HH1.
(* Goal: @eq (@Tpoint Tn) O X *)
(* Goal: @eq (@Tpoint Tn) O X *)
subst X.
(* Goal: @eq (@Tpoint Tn) O X *)
induction HH2.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
subst N.

(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction(col_dec O A B).
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(A = B \/ Midpoint O A B).
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply l7_20; Col.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction H15.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
contradiction.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(M = O).
(* Goal: @eq (@Tpoint Tn) O X *)
apply (l7_17 A B); auto.
(* Goal: @eq (@Tpoint Tn) O X *)
subst M; tauto.

(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction(col_dec O C D).
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(C = D \/ Midpoint O C D).
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply l7_20; Col.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction H16.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
contradiction.
(* Goal: @eq (@Tpoint Tn) O X *)
apply (l7_17 C D); auto.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(HM1:=mid_onc2__perp O P A B M H12 H H2 H3 H8).
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(HM2:=mid_onc2__perp O P C D M H12 H0 H4 H5 H9).
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: False *)
apply H1.
(* Goal: @Perp Tn O M Y X *)
(* Goal: @Col Tn X M Y *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
apply (l12_9_2D _ _ _ _ O M); Perp.

(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
apply perp_in_perp in H15.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction(col_dec O A B).
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(A = B \/ Midpoint O A B).
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply l7_20; Col.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction H17.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
contradiction.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(M = O).
(* Goal: @eq (@Tpoint Tn) O X *)
apply (l7_17 A B); auto.
(* Goal: @eq (@Tpoint Tn) O X *)
subst M; tauto.
(* Goal: @eq (@Tpoint Tn) O M *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(HM1:=mid_onc2__perp O P A B M H12 H H2 H3 H8).
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(perp_col M N C D O ) in H15; Col.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: False *)
apply H1.
(* Goal: @Perp Tn O M Y X *)
(* Goal: @Col Tn X M Y *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
apply (l12_9_2D _ _ _ _ O M); Perp.
(* Goal: @eq (@Tpoint Tn) O X *)
induction HH2.
(* Goal: @eq (@Tpoint Tn) O X *)
(* Goal: @eq (@Tpoint Tn) O X *)
subst X.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.

(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction(col_dec O C D).
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(C = D \/ Midpoint O C D).
(* Goal: or (@eq (@Tpoint Tn) C D) (@Midpoint Tn O C D) *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
unfold OnCircle in *.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply l7_20; Col.
(* Goal: @Cong Tn B A D C *)
(* Goal: @Cong Tn O N O M *)
apply cong_transitivity with O P; Cong.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
induction H17.
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
contradiction.
(* Goal: @eq (@Tpoint Tn) O X *)
apply (l7_17 C D); auto.

(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
assert(HM1:=mid_onc2__perp O P C D N H12 H0 H4 H5 H9).
(* Goal: @eq (@Tpoint Tn) O N *)
(* Goal: @eq (@Tpoint Tn) O X *)
apply perp_in_perp in H15.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: False *)
apply H1.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(perp_col N M A B O) in H15; Col.

(* Goal: @Perp Tn O M Y X *)
(* Goal: @Col Tn X M Y *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
apply (l12_9_2D _ _ _ _ O N); Perp.
(* Goal: @eq (@Tpoint Tn) O X *)
spliter.
(* Goal: @eq (@Tpoint Tn) O X *)
apply perp_in_perp in H17.
(* Goal: @eq (@Tpoint Tn) O X *)
apply perp_in_perp in H16.

(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(perp_col X M A B O) in H17; Col.
(* Goal: @Col Tn O C D *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
apply(perp_col X N C D O) in H16; Col.
(* Goal: @eq (@Tpoint Tn) O X *)
apply False_ind.
(* Goal: False *)
apply H1.
(* Goal: @Perp Tn O M Y X *)
(* Goal: @Col Tn X M Y *)
(* Goal: not (@eq (@Tpoint Tn) O M) *)
(* Goal: not (@eq (@Tpoint Tn) M X) *)
apply (l12_9_2D _ _ _ _ O X); Perp.
Qed.


End Circle_2D.