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

Require Import GeoCoq.Utils.all_equiv.

Section Elementary_Continuity_Props.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(**    All these properties are known to be equivalent in an arbitrary Hilbert plane (Tarski_2D)
  as shown by Strommer, but we don't have formalized the proof yet.

  We have the following proofs:
  - five equivalent variants of the circle-circle continuity axiom;
  - three equivalent variants of the line-circle continuity axiom;
  - the implication from the circle-circle continuity axiom to the line-circle continuity axiom.

  Since we have proved the circle-circle continuity axiom to follow from Tarski's axiom of continuity,
  all these properties do.
*)

Lemma segment_circle__one_point_line_circle : segment_circle <-> one_point_line_circle.
Proof.
(* Goal: iff (@segment_circle Tn) (@one_point_line_circle Tn) *)
  unfold segment_circle, one_point_line_circle.
(* Goal: and (@OnCircle Tn Z0 A B) (@OnCircle Tn Z0 C D) *)
  split.
  - intros Hsc A B U V P HCol HUV HBet.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      unfold InCircle, OnCircle in *.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@Cong Tn A Z A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      treat_equalities.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@Cong Tn A Z A A)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      exists A; Cong.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    assert (HPIn : InCircle P A B) by (apply bet__le1213; assumption).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (diff_col_ex3 U V P) as [W [HUW [HVW [HPW HCol2]]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (eq_dec_points A P).
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    { subst P.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      destruct (segment_construction W A A B) as [Q [HQ1 HQ2]].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      destruct (Hsc A B A Q) as [Z [HZ1 HZ2]]; trivial.
(* Goal: @OutCircle Tn Q A B *)
        apply cong__le; Cong.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      exists Z; split; trivial.
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
      ColR.
    }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (segment_construction W P P A) as [Q0 [HQ01 HQ02]].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (segment_construction P Q0 A B) as [Q [HQ1 HQ2]].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (Hsc A B P Q) as [Z [HZ1 HZ2]]; trivial.
(* Goal: @OutCircle Tn Q A B *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      apply (l5_6 Q Q0 Q A); Cong.
(* Goal: @Le Tn Q Q0 Q A *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      apply (triangle_reverse_inequality P); Cong.
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
      assert_diffs.
(* Goal: @Out Tn Z1 Z2 P *)
(* Goal: @Out Tn Q Z1 Z2 *)
      apply l6_6, bet_out; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    exists Z; split; trivial.
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
    ColR.

  - intros Hoplc A B P Q HPIn HQOut.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@Cong Tn A Z A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      unfold InCircle in HPIn; treat_equalities.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn A Z Q) (@OnCircle Tn Z A A)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
      exists A; split; Between; Circle.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (eq_dec_points P Q).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
      subst Q; exists P; split; Between; Circle.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
    destruct (cong_dec A B A Q) as [HCong|HNCong].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
      exists Q; split; Between; Circle.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
    assert (HB' : exists B', Cong A B A B' /\ Bet A P B').
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    { destruct (eq_dec_points A P).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Cong Tn A B A B') (@Bet Tn A P B')) *)
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Cong Tn A B A B') (@Bet Tn A P B')) *)
        subst; exists B; split; Cong; Between.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Cong Tn A B A B') (@Bet Tn A P B')) *)
      destruct (l6_11_existence A A B P) as [B' [HOut HCong]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Cong Tn A B A B') (@Bet Tn A P B')) *)
      exists B'; split; Cong.
(* Goal: @Bet Tn A P B' *)
      apply l6_13_1.
(* Goal: @Out Tn A P B' *)
(* Goal: @Le Tn A P A B' *)
        apply l6_6, HOut.
(* Goal: @Le Tn A D A B *)
(* Goal: and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) P P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
      apply (l5_6 A P A B); Cong.
    }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
    destruct HB' as [B' [HCong HBet]].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
    destruct (Hoplc A B' P Q P) as [Z1 [HCol1 HZ1]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
    assert (HZ1On: OnCircle Z1 A B) by (apply cong_transitivity with A B'; Cong).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
    clear dependent B'.
    destruct (or_bet_out P Z1 Q) as [HBet|[HOut|HNCol]];
      [exists Z1; auto| |exfalso; apply HNCol; Col].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
    destruct (chord_completion A B Z1 P) as [Z2 [HZ2On HBet]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Bet Tn P Z Q) (@OnCircle Tn Z A B)) *)
    exists Z2; split; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
    assert_diffs.
(* Goal: @Bet Tn P Z2 Q *)
    assert (HBet2 : Bet Z1 Z2 Q).
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    { apply out2__bet.
(* Goal: @Out Tn Z1 Z2 Q *)
(* Goal: @Out Tn Q Z1 Z2 *)
        apply l6_7 with P; trivial.
(* Goal: @Out Tn Z1 Z2 P *)
(* Goal: @Out Tn Q Z1 Z2 *)
        apply l6_6, bet_out; auto.
(* Goal: @Out Tn Q Z1 Z2 *)
      apply (col_inc2_outcs__out A B); Circle.
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
        ColR.
(* Goal: @OutCircleS Tn Q A B *)
      split; trivial.
    }
(* Goal: @Bet Tn P' Q Q' *)
(* Goal: @Bet Tn Q P' Q' *)
    eBetween.
Qed.

Lemma one_point_line_circle__two_points_line_circle :
  one_point_line_circle <-> two_points_line_circle.
Proof.
(* Goal: iff (@one_point_line_circle Tn) (@two_points_line_circle Tn) *)
  unfold one_point_line_circle, two_points_line_circle.
(* Goal: and (@OnCircle Tn Z0 A B) (@OnCircle Tn Z0 C D) *)
  split.
  - intros Hoplc A B U V P HCol HUV HBet.
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@Col Tn U V Z1) (and (@OnCircle Tn Z1 A B) (and (@Col Tn U V Z2) (and (@OnCircle Tn Z2 A B) (and (@Bet Tn Z1 P Z2) (forall _ : not (@eq (@Tpoint Tn) P B), not (@eq (@Tpoint Tn) Z1 Z2)))))))) *)
    destruct (eq_dec_points P B) as [Heq|HPB].
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@Col Tn U V Z1) (and (@OnCircle Tn Z1 A B) (and (@Col Tn U V Z2) (and (@OnCircle Tn Z2 A B) (and (@Bet Tn Z1 P Z2) (forall _ : not (@eq (@Tpoint Tn) P B), not (@eq (@Tpoint Tn) Z1 Z2)))))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@Col Tn U V Z1) (and (@OnCircle Tn Z1 A B) (and (@Col Tn U V Z2) (and (@OnCircle Tn Z2 A B) (and (@Bet Tn Z1 P Z2) (forall _ : not (@eq (@Tpoint Tn) P B), not (@eq (@Tpoint Tn) Z1 Z2)))))))) *)
      subst P; exists B, B; repeat split; Circle; Between.
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@Col Tn U V Z1) (and (@OnCircle Tn Z1 A B) (and (@Col Tn U V Z2) (and (@OnCircle Tn Z2 A B) (and (@Bet Tn Z1 P Z2) (forall _ : not (@eq (@Tpoint Tn) P B), not (@eq (@Tpoint Tn) Z1 Z2)))))))) *)
    destruct (Hoplc A B U V P HCol HUV HBet) as [Z1 [HZ1Col HZ1On]].
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
    exists Z1.
(* Goal: @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@Col Tn U V Z1) (and (@OnCircle Tn Z1 A B) (and (@Col Tn U V Z2) (and (@OnCircle Tn Z2 A B) (and (@Bet Tn Z1 P Z2) (forall _ : not (@eq (@Tpoint Tn) P B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
    assert (HPIn : InCircle P A B) by (apply bet__le1213, HBet).
(* Goal: @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@Col Tn U V Z1) (and (@OnCircle Tn Z1 A B) (and (@Col Tn U V Z2) (and (@OnCircle Tn Z2 A B) (and (@Bet Tn Z1 P Z2) (forall _ : not (@eq (@Tpoint Tn) P B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
    destruct (chord_completion A B Z1 P) as [Z2 [HZ2On HPBet]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@Col Tn U V Z1) (and (@OnCircle Tn Z1 A B) (and (@Col Tn U V Z2) (and (@OnCircle Tn Z2 A B) (and (@Bet Tn Z1 P Z2) (forall _ : not (@eq (@Tpoint Tn) P B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
    assert (Z1 <> P).
(* Goal: not (@eq (@Tpoint Tn) Z1 P) *)
(* Goal: @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@Col Tn U V Z1) (and (@OnCircle Tn Z1 A B) (and (@Col Tn U V Z2) (and (@OnCircle Tn Z2 A B) (and (@Bet Tn Z1 P Z2) (forall _ : not (@eq (@Tpoint Tn) P B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
      intro; treat_equalities; apply HPB, between_cong with A; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
    assert_diffs.
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
    exists Z2; repeat (split; trivial); ColR.

  - intros Htplc A B U V P HCol HUV HBet.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (Htplc A B U V P HCol HUV HBet) as [Z [_ [HZ1 [HZ2 _]]]].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    exists Z; auto.
Qed.


Lemma circle_circle_bis__circle_circle_axiom : circle_circle_bis <-> circle_circle_axiom.
Proof.
(* Goal: iff (@circle_circle_bis Tn) (@circle_circle_axiom Tn) *)
  split; intro cc.
  - intros A B C D B' D' HCong1 HCong2 HBet1 HBet2.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Cong Tn A Z A B) (@Cong Tn C Z C D)) *)
    apply cc with D' B'; try apply bet__le1213; trivial.
  - intros A B C D P Q HPOn HPIn HQOn HQIn.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    assert (HQ' : Le A P A Q) by (apply le_transitivity with A B; Le).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    apply l5_5_1 in HQ'.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct HQ' as [Q' [HBet1 HCong1]].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    assert (HP' : Le C Q C P) by (apply le_transitivity with C D; Le).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    apply l5_5_1 in HP'.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct HP' as [P' [HBet2 HCong2]].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (cc A Q' C P' Q P) as [Z []]; Cong.
(* Goal: and (@OnCircle Tn Z0 A B) (@OnCircle Tn Z0 C D) *)
    exists Z; split.
(* Goal: @OnCircle Tn Z A B *)
(* Goal: @OnCircle Tn Z C D *)
      apply cong_transitivity with A Q; [apply cong_transitivity with A Q'|]; Cong.
(* Goal: @OnCircle Tn Z C D *)
      apply cong_transitivity with C P; [apply cong_transitivity with C P'|]; Cong.
Qed.

Lemma circle_circle__circle_circle_bis : circle_circle -> circle_circle_bis.
Proof.
(* Goal: forall _ : @circle_circle Tn, @circle_circle_bis Tn *)
  intros Hcc A B C D P Q HPOn HPIn HQOn HQIn.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct (eq_dec_points P 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)) *)
    subst Q; exists P; split; assumption.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct (chord_completion C D P Q) as [P' [HP'On HBetQ]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct (chord_completion A B Q P) as [Q' [HQ'On HBetP]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  apply (Hcc A B C D P P'); trivial.
(* Goal: @OutCircle Tn P' A B *)
  destruct (le_cases A P' A B); trivial.
(* Goal: @OutCircle Tn P' A B *)
  assert (P' = Q).
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  { apply between_equality with Q'.
(* Goal: @Bet Tn P' Q Q' *)
(* Goal: @Bet Tn Q P' Q' *)
      eBetween.
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
    assert_diffs.
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
    apply (col_inc_onc2__bet A B); trivial; ColR.
  }
(* Goal: @OutCircle Tn P' A B *)
  subst.
(* Goal: @OutCircle Tn Q A B *)
  apply cong__le; Cong.
Qed.

Lemma circle_circle_bis__one_point_line_circle :
  circle_circle_bis -> one_point_line_circle.
Proof.
(* Goal: forall _ : @circle_circle_bis Tn, @one_point_line_circle Tn *)
  unfold circle_circle_bis, one_point_line_circle.
(* Goal: forall (_ : forall (A B C D P Q : @Tpoint Tn) (_ : @OnCircle Tn P C D) (_ : @InCircle Tn P A B) (_ : @OnCircle Tn Q A B) (_ : @InCircle Tn Q C D), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D))) (A B U V P : @Tpoint Tn) (_ : @Col Tn U V P) (_ : not (@eq (@Tpoint Tn) U V)) (_ : @Bet Tn A P B), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
  intro Hcc.
  assert (Haux : forall A B U V P, Col U V P -> U <> V -> Bet A P B -> ~ Per A U V ->
      exists Z : Tpoint, Col U V Z /\ OnCircle Z A B).
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  { intros A B U V P HCol HUV HBet HNPer.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (col_dec U V B) as [|HNCol].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z A D)) *)
      exists B; split; Circle.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (eq_dec_points A P).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      subst P.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      destruct (diff_col_ex3 U V A) as [W [HUW [HVW [HPW HCol2]]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      destruct (segment_construction W A A B) as [Z [HZ1 HZ2]].
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
      exists Z; split; trivial; ColR.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (l10_6_existence U V A) as [C HC].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (l10_6_existence U V B) as [D HD].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    assert (HBet' : Bet C P D).
(* Goal: @Bet Tn C P D *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      apply image_gen_preserves_bet with A P B U V; trivial.
(* Goal: @OutCircleS Tn Q A B *)
      left; split; trivial.
(* Goal: @ReflectL Tn P P U V *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      apply col__image_spec, HCol.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    assert (HCong : Cong B P D P) by (apply (is_image_col_cong U V); assumption).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    assert (HDIn : InCircle D A B).
(* Goal: @InCircle Tn B C D *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      apply triangle_inequality with P; Cong.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    assert (HBIn : InCircle B C D).
(* Goal: @InCircle Tn B C D *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
      apply triangle_inequality with P; Cong.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (Hcc A B C D D B) as [Z0 []]; Circle.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    destruct (circle_circle_cop A B C D Z0 U) as [Z [HZ1 [HZ2 HCop]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    clear dependent Z0.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    exists Z; split; trivial.
(* Goal: @Col Tn U V Z *)
    apply cong_cop_image__col with A C; trivial.
    - intro; treat_equalities.
(* Goal: False *)
(* Goal: False *)
      assert (Col A U V) by (apply l10_8, HC).
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
      apply HNCol; ColR.
    - apply cong_transitivity with A B; trivial.
(* Goal: @Cong Tn C P C Z1 *)
      apply cong_transitivity with C D; Cong.
(* Goal: @Cong Tn A B C D *)
      apply cong_symmetry, l10_10 with U V; assumption.
    - apply coplanar_perm_2.
(* Goal: @Coplanar Tn U A V Z *)
      apply coplanar_trans_1 with C; Cop.
(* Goal: not (@Col Tn C U A) *)
      intro.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
      destruct (eq_dec_points A C).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
        subst C.
(* Goal: False *)
(* Goal: False *)
        assert (Col A U V) by (apply l10_8, HC).
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
        apply HNCol; ColR.
(* Goal: False *)
      assert (Habs : ReflectL_at U A C U V).
(* Goal: @ReflectL_at Tn U A C U V *)
(* Goal: False *)
        apply image_image_in; Col.
(* Goal: @ReflectL Tn A C U V *)
(* Goal: False *)
        apply is_image_is_image_spec; auto.
(* Goal: False *)
      destruct Habs as [_ [|]]; auto.
(* Goal: False *)
      apply HNPer.
(* Goal: @Per Tn A U V *)
      destruct (eq_dec_points A U).
(* Goal: @Per Tn A U V *)
(* Goal: @Per Tn A U V *)
        subst; Perp.
(* Goal: @Per Tn A U V *)
      apply perp_per_2, perp_left_comm, perp_col with C; Perp; Col.
  }
(* Goal: forall (A B U V P : @Tpoint Tn) (_ : @Col Tn U V P) (_ : not (@eq (@Tpoint Tn) U V)) (_ : @Bet Tn A P B), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
  intros A B U V P HCol HUV HBet.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
  destruct (per_dec A U V); [|apply Haux with P; assumption].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
  destruct (Haux A B V U P) as [Z []]; Col.
(* Goal: not (@Per Tn A V U) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
    intro; apply HUV, l8_7 with A; assumption.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Col Tn U V Z) (@OnCircle Tn Z A B)) *)
  exists Z; split; Col.
Qed.

Lemma circle_circle__circle_circle_two :
 circle_circle <-> circle_circle_two.
Proof.
(* Goal: iff (@circle_circle Tn) (@circle_circle_two Tn) *)
  unfold circle_circle, circle_circle_two.
(* Goal: and (@OnCircle Tn Z0 A B) (@OnCircle Tn Z0 C D) *)
  split.
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  { intros Hcc A B C D P Q.
(* Goal: forall (_ : @OnCircle Tn P C D) (_ : @OnCircle Tn Q C D) (_ : @InCircle Tn P A B) (_ : @OutCircle Tn Q A B), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    destruct (eq_dec_points A C).
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    subst C.
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 A D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 A D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
      exists P; exists P.
(* Goal: and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) P P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
      assert (Cong A B A D).
(* Goal: @OnCircle Tn B A D *)
        apply le_anti_symmetry.
(* Goal: @Le Tn A B A D *)
(* Goal: @Le Tn A D A B *)
(* Goal: and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) P P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
        apply (l5_6 A B A Q); Cong.
(* Goal: @Le Tn A D A B *)
(* Goal: and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) P P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
        apply (l5_6 A P A B); Cong.
(* Goal: and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (and (@OnCircle Tn P A B) (and (@OnCircle Tn P A D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) P P))))) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
      assert (Cong A P A B) by (apply cong_transitivity with A D; Cong).
(* Goal: @OutCircleS Tn Q A B *)
      repeat split; trivial.
(* Goal: forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) P P) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
      intro Habs.
(* Goal: forall _ : @OutCircleS Tn Q A B, not (@eq (@Tpoint Tn) P P) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
      destruct Habs.
(* Goal: forall _ : @OutCircleS Tn Q A B, not (@eq (@Tpoint Tn) P P) *)
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
      contradiction.
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
    destruct (Hcc A B C D P Q) as [Z1 [HZ1A HZ1B]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))))) *)
    exists Z1.
(* Goal: @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2)))))) *)
    destruct (l10_6_existence A C Z1) as [Z2 HZ2].
(* Goal: @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2)))))) *)
    exists Z2.
(* Goal: and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))) *)
    assert (Cong Z1 C Z2 C) by (apply (is_image_col_cong A C Z1 Z2 C); Col).
(* Goal: and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2))))) *)
    assert (Cong Z1 A Z2 A) by (apply (is_image_col_cong A C Z1 Z2 A); Col).
(* Goal: @OutCircleS Tn Q A B *)
    repeat split; trivial.
(* Goal: @OnCircle Tn Z2 C D *)
(* Goal: forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2) *)
      unfold OnCircle in *; eCong.
(* Goal: @OnCircle Tn Z2 C D *)
(* Goal: forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2) *)
      unfold OnCircle in *; eCong.
(* Goal: forall (_ : @OnCircle Tn P C D) (_ : @OnCircle Tn Q C D) (_ : @InCircle Tn P A B) (_ : @OutCircle Tn Q A B), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) Z1 Z2) *)
    intro; subst Z2.
(* Goal: False *)
    clean.
(* Goal: False *)
    destruct (or_bet_out A C Z1) as [HBet|[HOut|HNCol]].
    - apply (lt__nle A B A Q); trivial.
(* Goal: @Le Tn A Q A B *)
      apply l5_6 with A Q A Z1; Cong.
(* Goal: @Le Tn A Q A Z1 *)
      apply triangle_inequality with C; trivial.
(* Goal: @Cong Tn C P C Z1 *)
      apply cong_transitivity with C D; Cong.
    - apply (lt__nle A P A B); trivial.
(* Goal: @Le Tn A B A P *)
      apply l5_6 with A Z1 A P; Cong.
(* Goal: @Le Tn A Z1 A P *)
      apply triangle_reverse_inequality with C; trivial.
(* Goal: @Cong Tn C P C Z1 *)
      apply cong_transitivity with C D; Cong.
    - assert (HCol := l10_8 A C Z1 HZ2); Col.
  }
(* Goal: forall (_ : forall (A B C D P Q : @Tpoint Tn) (_ : @OnCircle Tn P C D) (_ : @OnCircle Tn Q C D) (_ : @InCircle Tn P A B) (_ : @OutCircle Tn Q A B), @ex (@Tpoint Tn) (fun Z1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z2 : @Tpoint Tn => and (@OnCircle Tn Z1 A B) (and (@OnCircle Tn Z1 C D) (and (@OnCircle Tn Z2 A B) (and (@OnCircle Tn Z2 C D) (forall (_ : @InCircleS Tn P A B) (_ : @OutCircleS Tn Q A B), not (@eq (@Tpoint Tn) Z1 Z2)))))))) (A B C D P Q : @Tpoint Tn) (_ : @OnCircle Tn P C D) (_ : @OnCircle Tn Q C D) (_ : @InCircle Tn P A B) (_ : @OutCircle Tn Q A B), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  intros Hcct A B C D P Q.
(* Goal: forall (_ : @OnCircle Tn P C D) (_ : @OnCircle Tn Q C D) (_ : @InCircle Tn P A B) (_ : @OutCircle Tn Q A B), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  intros.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct (Hcct A B C D P Q) as [Z1 [Z2 [HZ1On [HZ1On' _]]]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  exists Z1; auto.
Qed.

Lemma euclid_22_aux : forall A B C D E F A' B' E' F' C1 C2 E1,
  SumS A B C D E' F' -> SumS C D E F A' B' -> Le E F E' F' -> Le A B A' B' ->
  Out A B C1 -> Cong A C1 C D -> Bet B A C2 -> Cong A C2 C D ->
  Out B A E1 -> Cong B E1 E F ->
  Bet C1 E1 C2.
Proof.
(* Goal: forall (_ : @OnCircle Tn P C D) (_ : @OnCircle Tn Q C D) (_ : @InCircle Tn P A B) (_ : @OutCircle Tn Q A B), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  intros A B C D E F A' B' E' F'; intros.
(* Goal: @Bet Tn C1 E1 C2 *)
  assert (Bet C1 A C2) by (assert_diffs; apply l6_2 with B; auto).
(* Goal: @Bet Tn C1 E1 C2 *)
  apply not_out_bet.
(* Goal: @Col Tn C1 E1 C2 *)
(* Goal: not (@Out Tn E1 C1 C2) *)
    ColR.
(* Goal: not (@Out Tn E1 C1 C2) *)
  intro HOut; destruct HOut as [HC1E1 [HC2E1 [HBet|HBet]]].
  - assert (Bet A C1 E1) by eBetween.
(* Goal: False *)
    assert (Bet A E1 B).
(* Goal: @Bet Tn A E1 B *)
(* Goal: False *)
      apply out2__bet; trivial.
(* Goal: @Out Tn A E1 B *)
(* Goal: False *)
      apply l6_7 with C1; apply l6_6; trivial.
(* Goal: @Out Tn A C1 E1 *)
(* Goal: False *)
      assert_diffs; apply bet_out; trivial.
(* Goal: False *)
    apply (le__nlt A B A' B'); trivial.
(* Goal: @Lt Tn A' B' A B *)
    apply le_lt12_sums2__lt with C D E F A E1 E1 B; Sums; Le.
(* Goal: and (@OnCircle Tn Z0 A B) (@OnCircle Tn Z0 C D) *)
    split.
(* Goal: @Le Tn C D A E1 *)
(* Goal: not (@Cong Tn C D A E1) *)
      exists C1; split; Cong.
(* Goal: not (@Cong Tn B C2 B E1) *)
(* Goal: @Cong Tn B C2 E' F' *)
    intro HCong.
(* Goal: False *)
    apply HC1E1, between_cong with A; trivial.
(* Goal: @Cong Tn A P E F *)
    apply cong_transitivity with C D; trivial.
  - assert (Bet A C2 E1) by eBetween.
(* Goal: False *)
    assert (Bet B C2 E1) by (assert_diffs; apply l6_2 with A; auto; apply bet_out; Between).
(* Goal: False *)
    apply (le__nlt E F E' F'); trivial.
(* Goal: @Lt Tn E' F' E F *)
    apply (cong2_lt__lt B C2 B E1); Cong.
(* Goal: @Lt Tn B C2 B E1 *)
(* Goal: @Cong Tn B C2 E' F' *)
      split; [exists C2; Cong|].
(* Goal: not (@Cong Tn B C2 B E1) *)
(* Goal: @Cong Tn B C2 E' F' *)
      intro HCong.
(* Goal: False *)
(* Goal: @Cong Tn B C2 E' F' *)
      apply HC2E1, between_cong with B; trivial.
(* Goal: @Cong Tn B C2 E' F' *)
    apply (sums2__cong56 A B C D); trivial; exists B, A, C2; repeat split; Cong.
Qed.

Lemma circle_circle_bis__euclid_22 : circle_circle_bis -> euclid_s_prop_1_22.
Proof.
(* Goal: forall _ : @circle_circle_bis Tn, @euclid_s_prop_1_22 Tn *)
  intros Hcc A B C D E F A' B' C' D' E' F' HSum1 HSum2 HSum3 HLe1 HLe2 HLe3.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn P Q A B) (and (@Cong Tn P R C D) (@Cong Tn Q R E F))))) *)
  exists A, B.
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
  destruct (eq_dec_points A B); [|destruct (eq_dec_points C D)]; [| |destruct (eq_dec_points E F)].
  - destruct (segment_construction_0 C D A) as [P HCong].
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
    exists P; repeat split; Cong.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
    subst B.
(* Goal: @Cong Tn A P E F *)
    apply cong_transitivity with C D; trivial.
(* Goal: @OnCircle Tn B A D *)
    apply le_anti_symmetry.
(* Goal: @Le Tn C D E F *)
(* Goal: @Le Tn E F C D *)
      apply (l5_6 C D C' D'); Cong; apply (sums2__cong56 A A E F); Sums.
(* Goal: @Le Tn E F C D *)
      apply (l5_6 E F E' F'); Cong; apply (sums2__cong56 A A C D); Sums.
  - exists A; treat_equalities; repeat split; Cong.
(* Goal: @OnCircle Tn B A D *)
    apply le_anti_symmetry.
(* Goal: @Le Tn B A E F *)
(* Goal: @Le Tn E F B A *)
      apply (l5_6 A B A' B'); Cong; apply (sums2__cong56 C C E F); Sums.
(* Goal: @Le Tn E F B A *)
      apply (l5_6 E F E' F'); Cong; apply (sums2__cong56 A B C C); Sums.
  - exists B; treat_equalities; repeat split; Cong.
(* Goal: @OnCircle Tn B A D *)
    apply le_anti_symmetry.
(* Goal: @Le Tn A B C D *)
(* Goal: @Le Tn C D A B *)
      apply (l5_6 A B A' B'); Cong; apply (sums2__cong56 C D E E); Sums.
(* Goal: @Le Tn C D A B *)
      apply (l5_6 C D C' D'); Cong; apply (sums2__cong56 A B E E); Sums.
  - destruct (segment_construction_3 A B C D) as [C1 [HC1 HC1']]; auto.
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
    destruct (segment_construction_3 B A E F) as [E1 [HE1 HE1']]; auto.
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
    destruct (segment_construction B A C D) as [C2 [HC2 HC2']].
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
    destruct (segment_construction A B E F) as [E2 [HE2 HE2']].
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
    assert (Bet C1 E1 C2) by (apply (euclid_22_aux A B C D E F A' B' E' F'); trivial).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
    assert (Bet E1 C1 E2) by (apply (euclid_22_aux B A E F C D B' A' C' D'); Sums; Le).
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
    destruct (Hcc A C1 B E1 E1 C1) as [Z [HZ1 HZ2]]; Circle.
(* Goal: @InCircle Tn E1 A C1 *)
(* Goal: @InCircle Tn C1 B E1 *)
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
      apply bet_inc2__inc with C1 C2; Circle; apply onc__inc, cong_transitivity with C D; Cong.
(* Goal: @InCircle Tn C1 B E1 *)
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
      apply bet_inc2__inc with E1 E2; Circle; apply onc__inc, cong_transitivity with E F; Cong.
(* Goal: @ex (@Tpoint Tn) (fun R : @Tpoint Tn => and (@Cong Tn A B A B) (and (@Cong Tn A R C D) (@Cong Tn B R E F))) *)
    exists Z; repeat split; Cong.
(* Goal: @Cong Tn A Z C D *)
(* Goal: @Cong Tn B Z E F *)
      apply cong_transitivity with A C1; Cong.
(* Goal: @Cong Tn B Z E F *)
      apply cong_transitivity with B E1; Cong.
Qed.

Lemma triangle_inequality1 : forall A B C D E, SumS A B B C D E -> Le A C D E.
Proof.
(* Goal: forall (A B C D E : @Tpoint Tn) (_ : @SumS Tn A B B C D E), @Le Tn A C D E *)
  intros A B C D E HSum.
(* Goal: @Le Tn A C D E *)
  destruct (segment_construction A B B C) as [D' [HBet HCong]].
(* Goal: @Le Tn A C D E *)
  apply (l5_6 A C A D'); Cong.
(* Goal: @Le Tn A C A D' *)
(* Goal: @Cong Tn A D' D E *)
    apply triangle_inequality with B; Cong.
(* Goal: @Cong Tn A D' D E *)
  apply (sums2__cong56 A B B C); trivial.
(* Goal: @SumS Tn A B B C A D' *)
  exists A, B, D'; repeat split; Cong.
Qed.

Lemma euclid_22__circle_circle : euclid_s_prop_1_22 -> circle_circle.
Proof.
(* Goal: forall _ : @euclid_s_prop_1_22 Tn, @circle_circle Tn *)
  intros p22 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 (HXYZ : exists X Y Z : Tpoint, Cong X Y A C /\ Cong X Z A B /\ Cong Y Z C D).
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  { destruct (ex_sums A B C D) as [L1 [R1]].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Cong Tn X Y A C) (and (@Cong Tn X Z A B) (@Cong Tn Y Z C D))))) *)
    destruct (ex_sums A C C D) as [L2 [R2]].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Cong Tn X Y A C) (and (@Cong Tn X Z A B) (@Cong Tn Y Z C D))))) *)
    destruct (ex_sums A C A B) as [L3 [R3]].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Cong Tn X Y A C) (and (@Cong Tn X Z A B) (@Cong Tn Y Z C D))))) *)
    apply p22 with L1 R1 L2 R2 L3 R3; trivial.
    - destruct (ex_sums C A A P) as [R [S]].
(* Goal: @Le Tn A C L1 R1 *)
      apply le_transitivity with R S.
(* Goal: @Le Tn C D R S *)
(* Goal: @Le Tn R S L3 R3 *)
        apply (l5_6 C P R S); Cong; apply triangle_inequality1 with A; trivial.
(* Goal: @Le Tn R S L3 R3 *)
        apply le2_sums2__le with C A A P A C A B; Le.
    - apply le_transitivity with A Q; Le.
(* Goal: @Le Tn A Q L2 R2 *)
      apply (triangle_inequality1 A C Q).
(* Goal: @SumS Tn A C C Q L2 R2 *)
      apply (cong3_sums__sums A C C D L2 R2); Cong.
    - destruct (ex_sums A P P C) as [R [S]].
(* Goal: @Le Tn A C L1 R1 *)
      apply le_transitivity with R S.
(* Goal: @Le Tn A C R S *)
(* Goal: @Le Tn R S L1 R1 *)
        apply triangle_inequality1 with P; trivial.
(* Goal: @Le Tn R S L1 R1 *)
      apply le2_sums2__le with A P P C A B C D; Le.
  }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct (eq_dec_points A C).
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  { subst C.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z A D)) *)
    exists B; split; Circle.
(* Goal: @OnCircle Tn B A D *)
    apply le_anti_symmetry.
(* Goal: @Le Tn A B A D *)
(* Goal: @Le Tn A D A B *)
      apply le_transitivity with A Q; Le.
(* Goal: @Le Tn A D A B *)
      apply le_transitivity with A P; Le.
  }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  { subst B.
(* Goal: @OutCircleS Tn Q A B *)
    exists P; split; trivial.
(* Goal: @OnCircle Tn P A A *)
    apply inc_eq in HPIn; subst; Circle.
  }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct HXYZ as [X [Y [Z [HAC [HAB HCD]]]]].
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  assert (HZ0 : exists Z0, CongA Y X Z C A Z0 /\ Cong X Z A Z0).
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  { destruct (angle_construction_3 Y X Z C A) as [Z']; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
    assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
    destruct (segment_construction_3 A Z' X Z) as [Z0 []]; auto.
(* Goal: @ex (@Tpoint Tn) (fun Z0 : @Tpoint Tn => and (@CongA Tn Y X Z C A Z0) (@Cong Tn X Z A Z0)) *)
    exists Z0; split; Cong.
(* Goal: @CongA Tn Y X Z C A Z0 *)
    apply out_conga with Y Z C Z'; [|apply out_trivial..|]; auto.
  }
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  destruct HZ0 as [Z0 []].
(* Goal: @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@OnCircle Tn Z A B) (@OnCircle Tn Z C D)) *)
  exists Z0.
(* Goal: and (@OnCircle Tn Z0 A B) (@OnCircle Tn Z0 C D) *)
  destruct (l11_49 Y X Z C A Z0); trivial.
(* Goal: and (@OnCircle Tn Z0 A B) (@OnCircle Tn Z0 C D) *)
  split.
(* Goal: @OnCircle Tn Z0 A B *)
(* Goal: @OnCircle Tn Z0 C D *)
    apply cong_transitivity with X Z; Cong.
(* Goal: @OnCircle Tn Z0 C D *)
    apply cong_transitivity with Y Z; Cong.
Qed.

Theorem equivalent_variants_of_circle_circle :
  all_equiv
    (circle_circle::
     circle_circle_two::
     circle_circle_bis::
     circle_circle_axiom::
     euclid_s_prop_1_22::
     nil).
Proof.
(* Goal: all_equiv (@cons Prop (@circle_circle Tn) (@cons Prop (@circle_circle_two Tn) (@cons Prop (@circle_circle_bis Tn) (@cons Prop (@circle_circle_axiom Tn) (@cons Prop (@euclid_s_prop_1_22 Tn) (@nil Prop)))))) *)
  assert (V := circle_circle_bis__circle_circle_axiom).
(* Goal: all_equiv (@cons Prop (@circle_circle Tn) (@cons Prop (@circle_circle_two Tn) (@cons Prop (@circle_circle_bis Tn) (@cons Prop (@circle_circle_axiom Tn) (@cons Prop (@euclid_s_prop_1_22 Tn) (@nil Prop)))))) *)
  assert (W := circle_circle__circle_circle_bis).
(* Goal: all_equiv (@cons Prop (@circle_circle Tn) (@cons Prop (@circle_circle_two Tn) (@cons Prop (@circle_circle_bis Tn) (@cons Prop (@circle_circle_axiom Tn) (@cons Prop (@euclid_s_prop_1_22 Tn) (@nil Prop)))))) *)
  assert (X := circle_circle__circle_circle_two).
(* Goal: all_equiv (@cons Prop (@circle_circle Tn) (@cons Prop (@circle_circle_two Tn) (@cons Prop (@circle_circle_bis Tn) (@cons Prop (@circle_circle_axiom Tn) (@cons Prop (@euclid_s_prop_1_22 Tn) (@nil Prop)))))) *)
  assert (Y := circle_circle_bis__euclid_22).
(* Goal: all_equiv (@cons Prop (@circle_circle Tn) (@cons Prop (@circle_circle_two Tn) (@cons Prop (@circle_circle_bis Tn) (@cons Prop (@circle_circle_axiom Tn) (@cons Prop (@euclid_s_prop_1_22 Tn) (@nil Prop)))))) *)
  assert (Z := euclid_22__circle_circle).
(* Goal: all_equiv (@cons Prop (@circle_circle Tn) (@cons Prop (@circle_circle_two Tn) (@cons Prop (@circle_circle_bis Tn) (@cons Prop (@circle_circle_axiom Tn) (@cons Prop (@euclid_s_prop_1_22 Tn) (@nil Prop)))))) *)
  apply all_equiv__equiv; unfold all_equiv'; simpl; repeat split; tauto.
Qed.

Theorem equivalent_variants_of_line_circle :
  all_equiv
    (segment_circle::
     one_point_line_circle::
     two_points_line_circle::
     nil).
Proof.
(* Goal: and (@OnCircle Tn Z0 A B) (@OnCircle Tn Z0 C D) *)
  apply all_equiv__equiv; unfold all_equiv'; simpl; repeat split.
(* Goal: forall _ : @two_points_line_circle Tn, @segment_circle Tn *)
(* Goal: forall _ : @segment_circle Tn, @one_point_line_circle Tn *)
(* Goal: forall _ : @one_point_line_circle Tn, @two_points_line_circle Tn *)
    rewrite segment_circle__one_point_line_circle, one_point_line_circle__two_points_line_circle; trivial.
(* Goal: forall _ : @segment_circle Tn, @one_point_line_circle Tn *)
(* Goal: forall _ : @one_point_line_circle Tn, @two_points_line_circle Tn *)
    rewrite segment_circle__one_point_line_circle; trivial.
(* Goal: forall _ : @one_point_line_circle Tn, @two_points_line_circle Tn *)
    rewrite one_point_line_circle__two_points_line_circle; trivial.
Qed.

End Elementary_Continuity_Props.
