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

Section Dedekind_circle_circle.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** This proof is inspired by Franz Rothe's proof of Theorem 8.5 in Several topics from geometry *)

Lemma circle_circle_aux : (forall A B C D P Q,
  OnCircle P C D -> OnCircle Q C D -> InCircleS P A B -> OutCircleS Q A B ->
  OS A C P Q \/ (Col P A C /\ ~ Col Q A C) \/ (~ Col P A C /\ Col Q A C ) ->
  exists Z : Tpoint, OnCircle Z A B /\ OnCircle Z C D) ->
  circle_circle.
Proof.
(* Goal: forall _ : forall (A B C D P Q : @Tpoint Tn) (_ : @OnCircle Tn P C D) (_ : @OnCircle Tn Q C D) (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B) (_ : or (@OS Tn A C P Q) (or (and (@Col Tn P A C) (not (@Col Tn Q A C))) (and (not (@Col Tn P A C)) (@Col Tn Q A C)))), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)), @circle_circle Tn *)
  intro Haux.
  cut (forall A B C D P Q,
  OnCircle P C D -> OnCircle Q C D -> InCircleS P A B -> OutCircleS Q A B ->
  Coplanar A C P Q -> (~ Col P A C \/ ~ Col Q A C) ->
  exists Z : Tpoint, OnCircle Z A B /\ OnCircle Z C D).
  - intros Haux' A B C D P Q HPOn HQOn HPIn HQOut.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    assert (HQ' : exists Q', OnCircle Q' C D /\ OutCircle Q' A B /\ Col Q' A C).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { destruct (segment_construction A C C D) as [Q' []].
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (@OnCircle Tn Q' C D) (and (@OutCircle Tn Q' A B) (@Col Tn Q' A C))) *)
      exists Q'.
(* Goal: and (@OnCircle Tn Q' C D) (and (@OutCircle Tn Q' A B) (@Col Tn Q' A C)) *)
      repeat split; Col.
(* Goal: @OutCircle Tn Q' A B *)
      apply le_transitivity with A Q; trivial.
(* Goal: @Le Tn A Q A Q' *)
      apply triangle_inequality with C; trivial.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
      apply cong_transitivity with C D; Cong.
    }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    clear dependent Q.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct HQ' as [Q [HQOn [HQOut HCol]]].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (cong_dec A P A B).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
      exists P; split; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (cong_dec A B A Q).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
      exists Q; Circle.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    assert (HPInS : InCircleS P A B) by (split; trivial).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    assert (HQOutS : OutCircleS Q A B) by (split; trivial).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    assert (A <> C).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { intro; subst C.
(* Goal: False *)
      apply (not_and_lt A B A P); split; trivial.
(* Goal: @Lt Tn A B A P *)
      apply (cong2_lt__lt A B A Q); Cong.
(* Goal: @Cong Tn A Q A P *)
      apply cong_transitivity with A D; Cong.
    }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    assert (C <> D).
(* Goal: not (@eq (@Tpoint Tn) C D) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
      intro; treat_equalities; apply (not_and_lt A C A B); split; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (col_dec P A C); [|apply Haux' with P Q; Cop].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (exists_cong_per A C C D) as [R [HR1 HR2]].
(* Goal: False *)
    assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    apply per_not_col in HR1; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (circle_cases A B R) as [HOn|HNOn].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
      exists R; split; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct HNOn; [apply Haux' with R Q|apply Haux' with P R]; Col; Cop.

  - intros A B C D P Q HPOn HQOn HPIn HQOut HCop HDij.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (col_dec P A C) as [HCol|HNCol].
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { destruct HDij.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
        contradiction.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
      apply Haux with P Q; auto.
    }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (col_dec Q A C).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
      apply Haux with P Q; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (cop__one_or_two_sides A C P Q); trivial; [|apply Haux with P Q; auto].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (l10_2_existence A C P) as [P' HP'].
(* Goal: False *)
    assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    apply Haux with P' Q; trivial.
(* Goal: @OnCircle Tn P' C D *)
(* Goal: @InCircleS Tn P' A B *)
(* Goal: or (@OS Tn A C P' Q) (or (and (@Col Tn P' A C) (not (@Col Tn Q A C))) (and (not (@Col Tn P' A C)) (@Col Tn Q A C))) *)
      apply cong_transitivity with C P; trivial.
(* Goal: @Cong Tn C P' C P *)
(* Goal: @InCircleS Tn P' A B *)
(* Goal: or (@OS Tn A C P' Q) (or (and (@Col Tn P' A C) (not (@Col Tn Q A C))) (and (not (@Col Tn P' A C)) (@Col Tn Q A C))) *)
      apply cong_commutativity, (is_image_col_cong A C); Col.
(* Goal: @InCircleS Tn P' A B *)
(* Goal: or (@OS Tn A C P' Q) (or (and (@Col Tn P' A C) (not (@Col Tn Q A C))) (and (not (@Col Tn P' A C)) (@Col Tn Q A C))) *)
      apply cong2_lt__lt with A P A B; Cong.
(* Goal: @Cong Tn A P A P' *)
(* Goal: or (@OS Tn A C P' Q) (or (and (@Col Tn P' A C) (not (@Col Tn Q A C))) (and (not (@Col Tn P' A C)) (@Col Tn Q A C))) *)
      apply cong_symmetry, cong_commutativity, (is_image_col_cong A C); Col.
(* Goal: or (@OS Tn A C P' Q) (or (and (@Col Tn P' A C) (not (@Col Tn Q A C))) (and (not (@Col Tn P' A C)) (@Col Tn Q A C))) *)
    left.
(* Goal: @OS Tn A C P' Q *)
    exists P; split; Side.
(* Goal: @TS Tn A C P' P *)
    apply l10_14; auto.
(* Goal: not (@eq (@Tpoint Tn) P' P) *)
    intro; subst; apply HNCol, l10_8, HP'.
Qed.

Lemma fod__circle_circle : first_order_dedekind -> circle_circle.
Proof.
(* Goal: forall _ : @first_order_dedekind Tn, @circle_circle Tn *)
  intro dedekind.
(* Goal: @circle_circle Tn *)
  apply circle_circle_aux.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @OnCircle Tn P C D) (_ : @OnCircle Tn Q C D) (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B) (_ : or (@OS Tn A C P Q) (or (and (@Col Tn P A C) (not (@Col Tn Q A C))) (and (not (@Col Tn P A C)) (@Col Tn Q A C)))), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  intros A B C D P Q HPOn HQOn HPIn HQOut HDij.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (A <> C).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
  { intro; subst C.
(* Goal: False *)
    apply (not_and_lt A B A P); split; trivial.
(* Goal: @Lt Tn A B A P *)
    apply (cong2_lt__lt A B A Q); Cong.
(* Goal: @Cong Tn A Q A P *)
    apply cong_transitivity with A D; Cong.
  }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (P <> Q) by (intro; apply (not_and_lt A P A B); subst; split; trivial).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (C <> D) by (intro; treat_equalities; auto).
  assert (HOS : forall X Y, Bet P X Q -> Bet P Y Q -> X <> P -> X <> Q -> Y <> P -> Y <> Q -> OS A C X Y).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
  { intros X Y; intros.
(* Goal: @OS Tn A C X Y *)
    destruct HDij as [HOS|[[HP HQ]|[HQ HP]]].
    - apply one_side_transitivity with P; [apply one_side_symmetry|]; apply l9_17 with Q; trivial.
    - apply one_side_transitivity with Q; [apply one_side_symmetry|];
(* Goal: @Out Tn A Z M *)
      apply out_one_side_1 with P; Col; apply l6_6, bet_out; auto.
    - apply one_side_transitivity with P; [apply one_side_symmetry|];
      apply out_one_side_1 with Q; Col; apply l6_6, bet_out; Between.
  }
  assert (HNTS : forall X Y, Bet P Y Q -> Bet P X Y -> ~ TS A C X Y).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
  { intros X Y HX HY HTS.
(* Goal: False *)
    absurd (TS A C P Q).
    - destruct HDij as [HOS'|[[HCol HNCol]|[HNCol HCol]]]; [apply l9_9_bis; trivial|intro..].
(* Goal: False *)
(* Goal: False *)
        apply (two_sides_not_col A C P Q); Col.
(* Goal: False *)
        apply (two_sides_not_col A C Q P); Col; Side.
    - destruct (eq_dec_points P X); destruct (eq_dec_points Q Y); treat_equalities; trivial.
(* Goal: @TS Tn A C P Q *)
(* Goal: @TS Tn A C P Q *)
(* Goal: @TS Tn A C P Q *)
        apply bet_ts__ts with Y; trivial.
(* Goal: @TS Tn A C P Q *)
(* Goal: @TS Tn A C P Q *)
        apply l9_2, bet_ts__ts with X; Side; Between.
(* Goal: @TS Tn A C P Q *)
(* Goal: @TS Tn A C P Q *)
        apply bet_ts__ts with Y; trivial; apply l9_2, bet_ts__ts with X; Side; Between.
  }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (HLta : LtA A C P A C Q).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
  { apply t18_19; Cong.
(* Goal: not (@eq (@Tpoint Tn) C Q) *)
(* Goal: @Cong Tn C Q C P *)
(* Goal: @Lt Tn P A Q A *)
      intro; treat_equalities; auto.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
      apply cong_transitivity with C D; Cong.
(* Goal: @Lt Tn P A Q A *)
      apply lt_comm, lt_transitivity with A B; trivial.
  }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (HNCol1 : ~ Col P Q C).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
  { intro.
    destruct HDij as [HOS'|[[HCol HNCol]|[HNCol HCol]]];
      [|apply HNCol; assert_diffs; ColR..].
(* Goal: False *)
    destruct HLta as [_ HNCongA].
(* Goal: False *)
    apply HNCongA, out2__conga.
(* Goal: @Out Tn C A A *)
(* Goal: @Out Tn C Q P *)
      apply out_trivial; auto.
(* Goal: @Out Tn C Q P *)
    apply col_one_side_out with A; Col; Side.
  }

  assert (Haux : forall X Y X0 Y0, Bet P Y Q -> X <> Y ->
    OnCircle X0 C D -> Out C X X0 -> OnCircle Y0 C D -> Out C Y Y0 -> Bet P X Y -> Lt A X0 A Y0).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
  { intros X Y X0 Y0; intros.
(* Goal: @Lt Tn A X0 A Y0 *)
    apply t18_18 with C C; Cong.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
      apply cong_transitivity with C D; Cong.
(* Goal: @LtA Tn X0 C A Y0 C A *)
    apply lta_comm, (conga_preserves_lta A C X A C Y).
(* Goal: @CongA Tn A C Y A C Y0 *)
(* Goal: @LtA Tn A C X A C Y *)
      apply out2__conga; [apply out_trivial|apply l6_6]; auto.
(* Goal: @CongA Tn A C Y A C Y0 *)
(* Goal: @LtA Tn A C X A C Y *)
      apply out2__conga; [apply out_trivial|apply l6_6]; auto.
(* Goal: @LtA Tn A C X A C Y *)
    split.
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { apply inangle__lea.
(* Goal: False *)
      assert_diffs.
(* Goal: @InAngle Tn X A C Y *)
      apply l11_24, in_angle_trans with P.
(* Goal: @Out Tn C A A *)
(* Goal: @Out Tn C Q P *)
        repeat split; auto; exists X; split; Between; right; apply out_trivial; auto.
(* Goal: @InAngle Tn P Y C A *)
      apply in_angle_trans2 with Q.
(* Goal: @InAngle Tn Y Q C P *)
(* Goal: @InAngle Tn P Q C A *)
        repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn Q X P) (or (@eq (@Tpoint Tn) X C) (@Out Tn C X Y))) *)
(* Goal: @InAngle Tn P Q C A *)
        exists Y; split; Between.
(* Goal: @Out Tn C A A *)
(* Goal: @Out Tn C Q P *)
        right; apply out_trivial; auto.
(* Goal: @InAngle Tn P Q C A *)
      destruct HDij as [HOS'|[[HCol HNCol]|[HNCol HCol]]].
      - apply l11_24, lea_in_angle; Lea; Side.
      - apply out341__inangle; auto.
(* Goal: @Out Tn C A P *)
        apply not_bet_out; Col.
(* Goal: not (@Out Tn C A Q) *)
        intro; apply (lta__nlea A C P A C Q); trivial.
(* Goal: @LeA Tn A C Q A C P *)
        apply l11_31_2; auto.
      - apply in_angle_line; auto.
(* Goal: @Bet Tn Q C A *)
        apply between_symmetry, not_out_bet; Col.
(* Goal: not (@Out Tn C A Q) *)
        intro; apply (lta__nlea A C P A C Q); trivial.
(* Goal: @LeA Tn A C Q A C P *)
        apply l11_31_1; auto.
    }
(* Goal: not (@Cong Tn A T A M) *)
    intro.
(* Goal: False *)
    destruct (conga_cop__or_out_ts A C X Y); trivial.
    - assert (Col P Q X) by ColR.
(* Goal: @Coplanar Tn A C X Y *)
      apply coplanar_pseudo_trans with P Q C; [assumption| |Cop..].
(* Goal: @Coplanar Tn P Q C A *)
      destruct HDij as [|[[]|[]]]; Cop.
    - absurd (X = Y); trivial; apply (l6_21 P Q C X); ColR.
    - apply (HNTS X Y); trivial.
  }

  assert (HR : exists R, forall X Y,
    (Bet P X Q /\ (exists X0, OnCircle X0 C D /\ Out C X X0 /\ InCircle X0 A B)) ->
    (Bet P Y Q /\ (exists Y0, OnCircle Y0 C D /\ Out C Y Y0 /\ OutCircle Y0 A B)) ->
    Bet X R Y).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
  { apply dedekind; [repeat constructor..|].
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => forall (X Y : @Tpoint Tn) (_ : and (@Bet Tn P X Q) (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@OnCircle Tn X0 C D) (and (@Out Tn C X X0) (@InCircle Tn X0 A B))))) (_ : and (@Bet Tn P Y Q) (@ex (@Tpoint Tn) (fun Y0 : @Tpoint Tn => and (@OnCircle Tn Y0 C D) (and (@Out Tn C Y Y0) (@OutCircle Tn Y0 A B))))), @Bet Tn A0 X Y) *)
    exists P.
(* Goal: forall (X Y : @Tpoint Tn) (_ : and (@Bet Tn P X Q) (@ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@OnCircle Tn X0 C D) (and (@Out Tn C X X0) (@InCircle Tn X0 A B))))) (_ : and (@Bet Tn P Y Q) (@ex (@Tpoint Tn) (fun Y0 : @Tpoint Tn => and (@OnCircle Tn Y0 C D) (and (@Out Tn C Y Y0) (@OutCircle Tn Y0 A B))))), @Bet Tn P X Y *)
    intros X Y [HX [X0]] [HY [Y0]].
(* Goal: @Bet Tn P X Y *)
    destruct (l5_3 P X Y Q); trivial.
(* Goal: @Bet Tn P X Y *)
    destruct (eq_dec_points X Y).
(* Goal: @Bet Tn P X Y *)
(* Goal: @Bet Tn P X Y *)
      subst; Between.
(* Goal: @Bet Tn P X Y *)
    exfalso.
(* Goal: False *)
    spliter.
(* Goal: False *)
    apply (lt__nle A Y0 A X0).
(* Goal: @Lt Tn A Y0 A X0 *)
(* Goal: @Le Tn A X0 A Y0 *)
      apply (Haux Y X); auto.
(* Goal: @Le Tn A X0 A Y0 *)
    apply le_transitivity with A B; trivial.
  }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (HP : exists X0, OnCircle X0 C D /\ Out C P X0 /\ InCircle X0 A B).
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@OnCircle Tn X0 C D) (and (@Out Tn C P X0) (@InCircle Tn X0 A B))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    exists P; repeat (split; Circle); apply out_trivial; assert_diffs; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (HQ : exists Y0, OnCircle Y0 C D /\ Out C Q Y0 /\ OutCircle Y0 A B).
(* Goal: @ex (@Tpoint Tn) (fun Y0 : @Tpoint Tn => and (@OnCircle Tn Y0 C D) (and (@Out Tn C Q Y0) (@OutCircle Tn Y0 A B))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    exists Q; repeat (split; Circle); apply out_trivial; assert_diffs; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct HR as [R HR].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (HBet : Bet P R Q) by (apply HR; split; Between).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (R <> C) by (intro; subst; apply HNCol1; Col).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct (onc_exists C D R) as [Z [HZ1 HZ2]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  exists Z; split; trivial.
(* Goal: @OnCircle Tn Z A B *)
  assert (A <> B) by (apply (lt_diff A P), HPIn).
(* Goal: @Bet Tn P X Y *)
  destruct (circle_cases A B Z) as [|[Habs|Habs]]; trivial; exfalso.


  - assert (Q <> R).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { intro; subst R.
(* Goal: False *)
      assert (Q = Z) by (apply (onc2_out__eq C D); trivial).
(* Goal: False *)
      subst.
(* Goal: False *)
      apply outcs__ninc in HQOut; Circle.
    }
(* Goal: False *)
    assert (HNCol2 : ~ Col C Q R) by (intro; apply HNCol1; ColR).
(* Goal: False *)
    assert (HT : exists T, OnCircle T A B /\ Bet A Z T).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { destruct (eq_dec_points Z A).
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@OnCircle Tn T A B) (@Bet Tn A Z T)) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@OnCircle Tn T A B) (@Bet Tn A Z T)) *)
        subst; exists B; split; Circle; Between.
(* Goal: False *)
      destruct (onc_exists A B Z) as [T [HT1 HT2]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@OnCircle Tn T A B) (@Bet Tn A Z T)) *)
      exists T; split; trivial.
(* Goal: @Bet Tn A Z T *)
      apply l6_13_1; trivial.
(* Goal: @Le Tn A Z A T *)
      apply (l5_6 A Z A B); Cong; Le.
    }
(* Goal: False *)
    destruct HT as [T [HT1 HT2]].
(* Goal: False *)
    assert (T <> Z).
(* Goal: not (@eq (@Tpoint Tn) T Z) *)
(* Goal: False *)
      intro; subst; apply incs__noutc in Habs; apply Habs; Circle.
(* Goal: False *)
    destruct (ex_per_cong C R Z Q T Z) as [I [HI1 [HI2 HI3]]]; Col.
(* Goal: False *)
    assert_diffs.
(* Goal: False *)
    assert (HNCol3 : ~ Col I Z C) by (apply per_not_col; auto).
(* Goal: False *)
    destruct (onc_exists C D I) as [X0 [HX0On HX0Out]]; auto.
(* Goal: False *)
    assert (HLt : Lt C X0 C I).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { destruct (l11_46 I Z C) as [_ HLt]; auto.
(* Goal: @Lt Tn C Y0 C I *)
        apply (cong2_lt__lt Z C I C); trivial.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
          apply cong_transitivity with C D; Cong.
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
          Cong.
    }
(* Goal: False *)
    assert (X0 <> I) by (intro; apply (nlt C I); subst; assumption).
(* Goal: False *)
    assert (HNCol4 : ~ Col I X0 Z) by (intro; apply (one_side_not_col123 C R I Q); ColR).
(* Goal: False *)
    assert (HLt1 : Lt X0 Z I Z).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { assert_diffs.
(* Goal: @Lt Tn X0 Z I Z *)
      destruct (l11_46 I X0 Z); auto.
(* Goal: or (@Per Tn I Y0 Z) (@Obtuse Tn I Y0 Z) *)
      right.
(* Goal: @Obtuse Tn I Y0 Z *)
      apply acute_bet__obtuse with C; auto.
(* Goal: @Bet Tn C Y0 I *)
(* Goal: @Acute Tn C Y0 Z *)
        apply l6_13_1; [apply l6_6|]; Le.
(* Goal: @Acute Tn C Y0 Z *)
      assert_diffs; apply cong__acute; auto.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
      apply cong_transitivity with C D; Cong.
    }

(* Goal: False *)
    assert (HX0In : InCircleS X0 A B).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { destruct (le_bet Z T Z X0) as [M [HM1 HM2]].
(* Goal: @Le Tn Z X0 Z T *)
(* Goal: @InCircleS Tn X0 A B *)
        apply (l5_6 X0 Z I Z); Cong; Le.
(* Goal: @InCircleS Tn X0 A B *)
      assert (HMT : M <> T).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
      { intro.
(* Goal: False *)
        apply (nlt Z M).
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
        apply (cong2_lt__lt X0 Z I Z); trivial; [|subst M; apply cong_transitivity with T Z]; Cong.
      }
(* Goal: @InCircleS Tn X0 A B *)
      apply le1234_lt__lt with A M.
      - apply triangle_inequality with Z; Cong; eBetween.
      - apply (cong2_lt__lt A M A T); Cong.
(* Goal: @Lt Tn A M A T *)
        assert (Bet A M T) by eBetween.
(* Goal: @Lt Tn A T A M *)
        split; Le.
(* Goal: not (@Cong Tn A T A M) *)
        intro.
(* Goal: False *)
        apply HMT, (between_cong A); assumption.
    }
(* Goal: False *)
    assert_diffs.
(* Goal: False *)
    assert (HX : InAngle X0 R C Q).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { apply l11_25 with X0 Z Q; try (apply out_trivial); auto.
(* Goal: @InAngle Tn X0 Z C Q *)
      apply lea_in_angle.
      - apply t18_19; auto.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
          apply cong_transitivity with C D; Cong.
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
          Cong.
(* Goal: @Lt Tn Y0 Z P Z *)
        apply le3456_lt__lt with I Z; trivial.
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
        apply (l5_6 T Z Q Z); Cong.
(* Goal: @Le Tn T Z Q Z *)
        assert (HLe : Le A T A Q) by (apply (l5_6 A B A Q); Cong; Le).
(* Goal: @Le Tn T Z Q Z *)
        destruct (eq_dec_points A Z).
(* Goal: @Le Tn T Z Q Z *)
(* Goal: @Le Tn T Z Q Z *)
          subst; Le.
(* Goal: @Le Tn T Z Q Z *)
        destruct (l5_5_1 A T A Q) as [M [HM1 HM2]]; trivial.
(* Goal: @Le Tn T Z Q Z *)
        assert (Bet A Z M) by eBetween.
(* Goal: @Le Tn T Z P Z *)
        apply le_transitivity with M Z.
(* Goal: @Le Tn T Z M Z *)
(* Goal: @Le Tn M Z P Z *)
          apply bet__le2313; eBetween.
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
        apply le_comm, (triangle_reverse_inequality A); Cong.
(* Goal: @Out Tn A Z M *)
        apply bet_out; auto.
      - apply invert_one_side, col_one_side with R; Col.
(* Goal: @OS Tn C R P Y0 *)
        apply one_side_transitivity with I; Side.
(* Goal: @OS Tn C R I Y0 *)
        apply out_one_side; trivial.
(* Goal: or (not (@Col Tn C R I)) (not (@Col Tn C R X0)) *)
        left; apply one_side_not_col123 with Q; trivial.
    }
(* Goal: False *)
    destruct HX as [_ [_ [_ [X [HX1 [HX2|HX2]]]]]].
(* Goal: False *)
(* Goal: False *)
      subst; apply HNCol2; Col.
(* Goal: False *)
    assert (X = R).
(* Goal: @eq (@Tpoint Tn) X R *)
(* Goal: False *)
      apply between_equality with Q; trivial.
(* Goal: @Bet Tn X R Q *)
(* Goal: False *)
      apply HR; split; [eBetween|..]; Between.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@OnCircle Tn X0 C D) (and (@Out Tn C X X0) (@InCircle Tn X0 A B))) *)
(* Goal: False *)
      exists X0; repeat (split; Circle).
(* Goal: False *)
    subst; apply HNCol4; ColR.


  - assert (P <> R).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { intro; subst R.
(* Goal: False *)
      assert (P = Z) by (apply (onc2_out__eq C D); trivial).
(* Goal: False *)
      subst.
(* Goal: False *)
      apply incs__noutc in HPIn; Circle.
    }
(* Goal: False *)
    assert (HNCol2 : ~ Col C P R) by (intro; apply HNCol1; ColR).
(* Goal: False *)
    destruct (onc_exists A B Z) as [T [HT1 HT2]]; auto.
(* Goal: not (@eq (@Tpoint Tn) Z A) *)
(* Goal: False *)
      apply (lt_diff A B), lt_right_comm, Habs.
(* Goal: False *)
    assert (HT3 : Bet A T Z).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { apply l6_13_1.
(* Goal: @Out Tn A T Z *)
(* Goal: @Le Tn A T A Z *)
        apply l6_6, HT2.
(* Goal: @Le Tn A T A Z *)
      apply (l5_6 A B A Z); Cong; Le.
    }
(* Goal: False *)
    assert (T <> Z).
(* Goal: not (@eq (@Tpoint Tn) T Z) *)
(* Goal: False *)
      intro; subst; apply outcs__ninc in Habs; apply Habs; Circle.
(* Goal: False *)
    destruct (ex_per_cong C R Z P T Z) as [I [HI1 [HI2 HI3]]]; Col.
(* Goal: False *)
    assert_diffs.
(* Goal: False *)
    assert (HNCol3 : ~ Col I Z C) by (apply per_not_col; auto).

(* Goal: False *)
    destruct (onc_exists C D I) as [Y0 [HY0On HY0Out]]; auto.
(* Goal: False *)
    assert (HLt : Lt C Y0 C I).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { destruct (l11_46 I Z C) as [_ HLt]; auto.
(* Goal: @Lt Tn C Y0 C I *)
        apply (cong2_lt__lt Z C I C); trivial.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
          apply cong_transitivity with C D; Cong.
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
          Cong.
    }
(* Goal: False *)
    assert (Y0 <> I) by (intro; apply (nlt C I); subst; assumption).
(* Goal: False *)
    assert (HNCol4 : ~ Col I Y0 Z) by (intro; apply (one_side_not_col123 C R I P); ColR).
(* Goal: False *)
    assert (HLt1 : Lt Y0 Z I Z).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { assert_diffs.
(* Goal: @Lt Tn Y0 Z I Z *)
      destruct (l11_46 I Y0 Z); auto.
(* Goal: or (@Per Tn I Y0 Z) (@Obtuse Tn I Y0 Z) *)
      right.
(* Goal: @Obtuse Tn I Y0 Z *)
      apply acute_bet__obtuse with C; auto.
(* Goal: @Bet Tn C Y0 I *)
(* Goal: @Acute Tn C Y0 Z *)
        apply l6_13_1; [apply l6_6|]; Le.
(* Goal: @Acute Tn C Y0 Z *)
      assert_diffs; apply cong__acute; auto.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
      apply cong_transitivity with C D; Cong.
    }

(* Goal: False *)
    assert (HY0OutC : OutCircleS Y0 A B).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { destruct (le_bet Z T Z Y0) as [M [HM1 HM2]].
(* Goal: @Le Tn Z Y0 Z T *)
(* Goal: @OutCircleS Tn Y0 A B *)
        apply (l5_6 Y0 Z I Z); Cong; Le.
(* Goal: @OutCircleS Tn Y0 A B *)
      assert (HTM : T <> M).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
      { intro.
(* Goal: False *)
        apply (nlt Z M).
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
        apply (cong2_lt__lt Y0 Z I Z); trivial; [|subst M; apply cong_transitivity with T Z]; Cong.
      }
(* Goal: @OutCircleS Tn Y0 A B *)
      apply le3456_lt__lt with A M.
      - apply (cong2_lt__lt A T A M); Cong.
(* Goal: @Lt Tn A T A M *)
        assert (Bet A T M) by eBetween.
(* Goal: @Lt Tn A T A M *)
        split; Le.
(* Goal: not (@Cong Tn A T A M) *)
        intro.
(* Goal: False *)
        apply HTM, (between_cong A); assumption.
      - apply (triangle_reverse_inequality Z); Cong.
(* Goal: @Out Tn Z A M *)
        assert_diffs; apply l6_6, bet_out; eBetween.
    }
(* Goal: False *)
    assert_diffs.
(* Goal: False *)
    assert (HY : InAngle Y0 P C R).
(* Goal: @InAngle Tn Y0 P C R *)
(* Goal: False *)
    { apply l11_25 with Y0 P Z; try (apply out_trivial); auto.
(* Goal: @InAngle Tn Y0 P C Z *)
      apply l11_24, lea_in_angle.
      - apply t18_19; auto.
(* Goal: @Cong Tn C P C Y0 *)
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
          apply cong_transitivity with C D; Cong.
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
          Cong.
(* Goal: @Lt Tn Y0 Z P Z *)
        apply le3456_lt__lt with I Z; trivial.
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
        apply (l5_6 T Z P Z); Cong.
(* Goal: @Le Tn T Z P Z *)
        destruct (le_bet A T A P) as [M [HM1 HM2]].
(* Goal: @Le Tn A P A T *)
(* Goal: @Le Tn T Z P Z *)
          apply (l5_6 A P A B); Cong; Le.
(* Goal: @Le Tn T Z P Z *)
        assert (Bet A M Z) by eBetween.
(* Goal: @Le Tn T Z P Z *)
        destruct (eq_dec_points M A).
(* Goal: @Le Tn T Z P Z *)
(* Goal: @Le Tn T Z P Z *)
          treat_equalities; Le.
(* Goal: @Le Tn T Z P Z *)
        apply le_transitivity with M Z.
(* Goal: @Le Tn T Z M Z *)
(* Goal: @Le Tn M Z P Z *)
          apply bet__le2313; eBetween.
(* Goal: @Cong Tn C Z C Z *)
(* Goal: @Lt Tn Y0 Z P Z *)
        apply le_comm, (triangle_reverse_inequality A); Cong.
(* Goal: @Out Tn A Z M *)
        apply l6_6, bet_out; auto.
      - apply invert_one_side, col_one_side with R; Col.
(* Goal: @OS Tn C R P Y0 *)
        apply one_side_transitivity with I; Side.
(* Goal: @OS Tn C R I Y0 *)
        apply out_one_side; trivial.
(* Goal: or (not (@Col Tn C R I)) (not (@Col Tn C R Y0)) *)
        left; apply one_side_not_col123 with P; trivial.
    }
(* Goal: False *)
    destruct HY as [_ [_ [_ [Y [HY1 [HY2|HY2]]]]]].
(* Goal: False *)
(* Goal: False *)
      subst; apply HNCol2; Col.
(* Goal: False *)
    assert (Y = R).
(* Goal: @eq (@Tpoint Tn) Y R *)
(* Goal: False *)
      apply between_equality with P; apply between_symmetry; trivial.
(* Goal: @Bet Tn P R Y *)
(* Goal: False *)
      apply HR; split; [Between..| |]; [eBetween|].
(* Goal: @ex (@Tpoint Tn) (fun Y0 : @Tpoint Tn => and (@OnCircle Tn Y0 C D) (and (@Out Tn C Y Y0) (@OutCircle Tn Y0 A B))) *)
(* Goal: False *)
      exists Y0; repeat (split; Circle).
(* Goal: False *)
    subst; apply HNCol4; ColR.
Qed.

End Dedekind_circle_circle.