Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Meta_theory.Continuity.first_order.
Require Import GeoCoq.Meta_theory.Continuity.first_order_dedekind_circle_circle.
Require Import GeoCoq.Meta_theory.Continuity.elementary_continuity_props.
Require Import GeoCoq.Tarski_dev.Ch05_bet_le.

Section Tarski_continuous_to_TRC.

Context `{TC:Tarski_continuous}.

Instance TC_to_TRC : Tarski_ruler_and_compass TnEQD.
Proof.
(* Goal: @Tarski_ruler_and_compass Tn TnEQD *)
  split.
(* Goal: forall (A B C D B' D' : @Tpoint Tn) (_ : @Cong Tn A B' A B) (_ : @Cong Tn C D' C D) (_ : @Bet Tn A D' B) (_ : @Bet Tn C B' D), @ex (@Tpoint Tn) (fun Z : @Tpoint Tn => and (@Cong Tn A Z A B) (@Cong Tn C Z C D)) *)
  apply circle_circle_bis__circle_circle_axiom, circle_circle__circle_circle_bis, fod__circle_circle, dedekind__fod.
(* Goal: @dedekind_s_axiom Tn *)
  unfold dedekind_s_axiom.
(* Goal: forall (Alpha Beta : forall _ : @Tpoint Tn, Prop) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => forall (X Y : @Tpoint Tn) (_ : Alpha X) (_ : Beta Y), @Bet Tn A X Y)), @ex (@Tpoint Tn) (fun B : @Tpoint Tn => forall (X Y : @Tpoint Tn) (_ : Alpha X) (_ : Beta Y), @Bet Tn X B Y) *)
  exact continuity.
Defined.

End Tarski_continuous_to_TRC.