Require Import GeoCoq.Axioms.tarski_axioms.
Require Import GeoCoq.Elements.OriginalProofs.proposition_01.
Require Import GeoCoq.Elements.OriginalProofs.lemma_congruenceflip.
Require Import GeoCoq.Elements.OriginalProofs.lemma_extension.
Require Import Classical.

Section Euclid_to_Tarski.

Context `{Ax:euclidean_neutral_ruler_compass}.

Definition Bet A B C := BetS A B C \/ A=B \/ B=C.

Lemma Bet_sym : forall A B C,
  Bet A B C -> Bet C B A.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: @Logic.eq (@Point Ax0) A B *)
unfold Bet in *.
(* Goal: or (@BetS Ax0 C B A) (or (@Logic.eq (@Point Ax0) C B) (@Logic.eq (@Point Ax0) B A)) *)
decompose [or] H.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
left.
(* Goal: @BetS Ax0 C B A *)
(* Goal: or (@BetS Ax0 C B A) (or (@Logic.eq (@Point Ax0) C B) (@Logic.eq (@Point Ax0) B A)) *)
(* Goal: or (@BetS Ax0 C B A) (or (@Logic.eq (@Point Ax0) C B) (@Logic.eq (@Point Ax0) B A)) *)
eauto using axiom_betweennesssymmetry.
(* Goal: or (@BetS Ax0 C B A) (or (@Logic.eq (@Point Ax0) C B) (@Logic.eq (@Point Ax0) B A)) *)
(* Goal: or (@BetS Ax0 C B A) (or (@Logic.eq (@Point Ax0) C B) (@Logic.eq (@Point Ax0) B A)) *)
right;right;auto.
(* Goal: or (@BetS Ax0 C B A) (or (@Logic.eq (@Point Ax0) C B) (@Logic.eq (@Point Ax0) B A)) *)
right;left;auto.
Qed.

Definition TCong A B C D := Cong A B C D \/ (A=B /\ C=D).

Lemma cong_sym : forall A B C D, Cong A B C D -> Cong C D A B.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: @Cong Ax0 C D A B *)
apply (cn_congruencetransitive C D A B A B).
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
assumption.
(* Goal: @Cong Ax0 A B A B *)
apply (cn_congruencereflexive).
Qed. 

Lemma cong_eq : forall A B C, Cong B C A A -> B=C.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: @Logic.eq (@Point Ax0) B C *)
destruct (classic (B=C)).
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
assumption.
(* Goal: @Logic.eq (@Point Ax0) B C *)
assert (A<>A).
(* Goal: not (@Logic.eq (@Point Ax0) A A) *)
(* Goal: @Logic.eq (@Point Ax0) B C *)
apply axiom_nocollapse with B C;auto.
(* Goal: False *)
intuition.
Qed.

Lemma nullsegment2 : forall A B, TCong A A B B.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: TCong B X C D *)
unfold TCong;auto.
Qed.

Lemma Tcong_reflexive: forall A B, TCong A B A B.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
unfold TCong.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
left.
(* Goal: @Cong Ax0 A B A B *)
apply cn_congruencereflexive.
Qed.

Lemma Tcong_symmetric: forall A B C D, TCong A B C D -> TCong C D A B.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: @Logic.eq (@Point Ax0) A B *)
unfold TCong in *.
destruct  H.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
left.
(* Goal: @Cong Ax0 C D A B *)
(* Goal: or (@Cong Ax0 C D A B) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) A B)) *)
apply cong_sym.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
assumption.
(* Goal: False *)
right;intuition.
Qed.

Lemma nullsegment1 : forall A B C, TCong A A B C -> B=C.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: @Logic.eq (@Point Ax0) A B *)
unfold TCong in *.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
destruct H.
(* Goal: or (@Cong Ax0 C D F F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) F F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
apply cong_sym in H.
(* Goal: or (@Cong Ax0 C D F F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) F F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
apply cong_eq in H.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
assumption.
(* Goal: False *)
intuition.
Qed.

Lemma TCong_neq_Cong : forall A B C D, A<>B -> TCong A B C D -> Cong A B C D.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
destruct H0.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
assumption.
(* Goal: False *)
intuition.
Qed.

Lemma lemma_congruenceflip : 
   forall A B C D, 
   Cong A B C D ->
   Cong B A D C.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
intros.
(* Goal: @Cong Ax0 B A D C *)
assert (Cong B A A B) by (auto using cn_equalityreverse).
(* Goal: @Cong Ax0 B A D C *)
assert (Cong C D D C) by (auto using cn_equalityreverse).
(* Goal: @Cong Ax0 B A D C *)
assert (Cong B A C D) by (conclude lemma_congruencetransitive).
(* Goal: @Cong Ax0 B A D C *)
conclude lemma_congruencetransitive.
Qed.


Instance Tarski_follows_Euclid: Tarski_neutral_dimensionless.
Proof.
(* Goal: Tarski_neutral_dimensionless *)
eapply (Build_Tarski_neutral_dimensionless Point Bet TCong) with (PA:=PA) (PB:=PB) (PC:=PC).
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
- intros.
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  unfold TCong.
(* Goal: or (@Cong Ax0 A B B A) (and (@Logic.eq (@Point Ax0) A B) (@Logic.eq (@Point Ax0) B A)) *)
  left; apply cn_equalityreverse.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
- intros.
(* Goal: @Logic.eq (@Point Ax0) A B *)
  unfold TCong in *.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  destruct H;destruct H0.
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  left;apply cn_congruencetransitive with A B;auto.
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  spliter;subst.
(* Goal: or (@Cong Ax0 C D F F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) F F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  apply cong_sym in H.
(* Goal: or (@Cong Ax0 C D F F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) F F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  apply cong_eq in H.
(* Goal: or (@Cong Ax0 D D E F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  subst;auto.
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  spliter;subst.
(* Goal: or (@Cong Ax0 D D E F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
   apply cong_sym in H0.
(* Goal: or (@Cong Ax0 D D E F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  apply cong_eq in H0.
(* Goal: or (@Cong Ax0 D D E F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) E F)) *)
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  subst;auto.
(* Goal: or (@Cong Ax0 C D E F) (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) E F)) *)
  spliter;subst.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  auto.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
- intros.
(* Goal: @Logic.eq (@Point Ax0) A B *)
  unfold TCong in *.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  destruct H.
(* Goal: @Logic.eq (@Point Ax0) A B *)
(* Goal: @Logic.eq (@Point Ax0) A B *)
  apply cong_eq with C.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  assumption.
(* Goal: False *)
  intuition.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
- intros.
(* Goal: @ex (@Point Ax0) (fun E : @Point Ax0 => and (Bet A B E) (TCong B E C D)) *)
  elim (classic (C=D));intro.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  subst.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  exists B.
(* Goal: and (Bet P C B) (Bet Q C A) *)
  split.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  unfold Bet;auto.
(* Goal: TCong B B D D *)
(* Goal: @ex (@Point Ax0) (fun E : @Point Ax0 => and (Bet A B E) (TCong B E C D)) *)
  apply nullsegment2.
(* Goal: @ex (@Point Ax0) (fun E : @Point Ax0 => and (Bet A B E) (TCong B E C D)) *)
  elim (classic (A=B));intro.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  subst.
(* Goal: TCong C D C' D' *)
  elim (classic (B=C));intro.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  * subst.
(* Goal: @ex (@Point Ax0) (fun E : @Point Ax0 => and (Bet C C E) (TCong C E C D)) *)
    exists D.
(* Goal: and (Bet P C B) (Bet Q C A) *)
    split.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
    unfold Bet;right;auto.
(* Goal: TCong C D C D *)
    apply Tcong_reflexive.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  * destruct (lemma_extension  C B C D) as [X [HXA HXB]];unfold neq;auto.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
    exists X.
(* Goal: and (Bet P C B) (Bet Q C A) *)
    split.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
    unfold Bet;right;auto.
(* Goal: TCong B X C D *)
    unfold TCong;auto.
  * destruct (lemma_extension A B C D) as [X [HXA HXB]];
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  unfold neq;auto.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  exists X.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  unfold Bet, TCong;auto. 
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
- intros.
(* Goal: TCong C D C' D' *)
  elim (classic (B=C));intro.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  subst.
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  assert (B'=C'). 
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  apply nullsegment1 with C;assumption.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  subst.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  assumption.
(* Goal: TCong C D C' D' *)
  assert (B'<>C').
(* Goal: not (@Logic.eq (@Point Ax0) A' D') *)
(* Goal: TCong C D C' D' *)
  {
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  intro;subst.
(* Goal: False *)
  apply H6.
(* Goal: @Logic.eq (@Point Ax0) B C *)
  apply nullsegment1 with C'.
(* Goal: TCong D' D' A D *)
  apply Tcong_symmetric.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  assumption.
  }
(* Goal: TCong C D C' D' *)
  assert (A'<>B').
(* Goal: not (@Logic.eq (@Point Ax0) A' D') *)
(* Goal: TCong C D C' D' *)
  {
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  intro;subst.
(* Goal: False *)
  apply H5.
(* Goal: @Logic.eq (@Point Ax0) A B *)
  apply nullsegment1 with B'.
(* Goal: TCong D' D' A D *)
  apply Tcong_symmetric.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  assumption.
  }
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
 apply TCong_neq_Cong in H0;auto.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
 apply TCong_neq_Cong in H;auto.
(* Goal: TCong C D C' D' *)
 destruct (classic (A=D)).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
 * subst.
(* Goal: TCong C D C' D' *)
   assert (A'=D') by (apply nullsegment1 with D;auto).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
   subst.
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
   unfold TCong.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
   left.
(* Goal: @Cong Ax0 C D C' D' *)
   apply cn_sumofparts with B B'.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
   apply lemma_congruenceflip;auto.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
   apply lemma_congruenceflip;auto.
(* Goal: @BetS Ax0 C B D *)
(* Goal: @BetS Ax0 C' B' D' *)
   unfold Bet in H3.
(* Goal: @BetS Ax0 C' B' D' *)
   apply axiom_betweennesssymmetry.
(* Goal: False *)
   destruct H3;intuition.
(* Goal: @BetS Ax0 C' B' D' *)
   apply axiom_betweennesssymmetry.
(* Goal: False *)
   destruct H4;intuition.
 * assert (A'<>D').
(* Goal: not (@Logic.eq (@Point Ax0) A' D') *)
(* Goal: TCong C D C' D' *)
  {
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  intro;subst.
(* Goal: False *)
  apply H9.
(* Goal: @Logic.eq (@Point Ax0) A D *)
  apply nullsegment1 with D'.
(* Goal: TCong D' D' A D *)
  apply Tcong_symmetric.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  assumption.
  }
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  apply TCong_neq_Cong in H1;auto.
(* Goal: TCong C D C' D' *)
  destruct (classic (B=D)).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  subst.
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  assert (B'=D').
(* Goal: @Logic.eq (@Point Ax0) B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  apply nullsegment1 with D.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  assumption.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  subst.
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  unfold TCong.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
  left.
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
  apply lemma_congruenceflip;assumption.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
 apply TCong_neq_Cong in H2;auto.
(* Goal: TCong C D C' D' *)
 assert (Cong D C D' C').
(* Goal: TCong D D B' D' *)
(* Goal: TCong C D C' D' *)
(* Goal: TCong C D C' D' *)
 apply (axiom_5_line A B C D A' B' C' D' H0 H1 H2);try assumption.
(* Goal: @Logic.eq (@Point Ax0) A B *)
 unfold Bet in *.
(* Goal: False *)
 intuition.
(* Goal: @Logic.eq (@Point Ax0) A B *)
 unfold Bet in *.
(* Goal: False *)
 intuition.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
 unfold TCong;left.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
 apply (lemma_congruenceflip);auto.
(* Goal: forall (A B : @Point Ax0) (_ : Bet A B A), @Logic.eq (@Point Ax0) A B *)
- intros.
(* Goal: @Logic.eq (@Point Ax0) A B *)
  unfold Bet in *.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  destruct H.
(* Goal: @Logic.eq (@Point Ax0) A B *)
(* Goal: @Logic.eq (@Point Ax0) A B *)
  exfalso.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  apply (axiom_betweennessidentity A B);auto.
(* Goal: False *)
  intuition.
- intros A B C P Q H H0.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  destruct H.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  destruct H0.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  elim (classic (Col A B C));intro.
  unfold Col in *.
  decompose [or] H1;clear H1;
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  unfold eq in *;subst.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  * exists B;split;unfold Bet;auto.
  * exfalso; apply lemma_betweennotequal in H.
    unfold neq,eq in *;spliter.
(* Goal: False *)
    intuition.
  * exfalso;apply lemma_betweennotequal in H0.
(* Goal: False *)
    unfold neq,eq in *;intuition.
  * exists A.
(* Goal: and (Bet P C B) (Bet Q C A) *)
  split.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
  unfold Bet;left. 
(* Goal: @BetS Ax0 Q C A *)
  eauto using lemma_3_6a, axiom_betweennesssymmetry.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  unfold Bet;auto.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  * exists B.
(* Goal: and (Bet P C B) (Bet Q C A) *)
  split.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  unfold Bet;auto.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
  unfold Bet;left.
(* Goal: @BetS Ax0 Q C A *)
  eauto using lemma_3_6a, axiom_betweennesssymmetry.
  * exists C.
(* Goal: and (Bet P C B) (Bet Q C A) *)
  split.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
  unfold Bet;left.
(* Goal: @BetS Ax0 Q C A *)
  eauto using lemma_3_6a, axiom_betweennesssymmetry.
(* Goal: or (@Cong Ax0 C D C' D') (and (@Logic.eq (@Point Ax0) C D) (@Logic.eq (@Point Ax0) C' D')) *)
(* Goal: TCong C D C' D' *)
  unfold Bet;left.
(* Goal: @BetS Ax0 Q C A *)
  eauto using lemma_3_6a, axiom_betweennesssymmetry.
  * assert (T:exists X : Point, BetS A X Q /\ BetS B X P).
   apply  (postulate_Pasch_inner A B C P Q H H0).
(* Goal: @nCol Ax0 A C B *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
   unfold nCol,neq.
   unfold Col in *.
  assert (BetS B A C <-> BetS C A B)
     by (split;intro;apply axiom_betweennesssymmetry;auto).
  assert (eq C B <-> eq B C) by (split;unfold eq;intro;auto).
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  tauto.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  destruct T as [X [HXA HXB]].
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  exists X.
(* Goal: and (Bet P X B) (Bet Q X A) *)
  split;unfold Bet;left;auto using axiom_betweennesssymmetry.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  * destruct H0.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  subst.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  exists Q;unfold Bet;auto.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  subst.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet C X A)) *)
  exists P.
(* Goal: and (Bet P P B) (Bet C P A) *)
  unfold Bet;auto using axiom_betweennesssymmetry.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (Bet P X B) (Bet Q X A)) *)
  * destruct H.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  subst;exists P; unfold Bet;auto.
(* Goal: and (Bet P C B) (Bet Q C A) *)
  subst;exists Q;split.
(* Goal: Bet C Q B *)
(* Goal: Bet Q Q A *)
  auto using Bet_sym.
(* Goal: or (@Cong Ax0 D D F F) (and (@Logic.eq (@Point Ax0) D D) (@Logic.eq (@Point Ax0) F F)) *)
  unfold Bet;auto.
- assert (T:=axiom_lower_dim).
  unfold nCol,Bet,neq,eq in *.
(* Goal: not (or (or (@BetS Ax0 (@PA Ax0) (@PB Ax0) (@PC Ax0)) (or (@Logic.eq (@Point Ax0) (@PA Ax0) (@PB Ax0)) (@Logic.eq (@Point Ax0) (@PB Ax0) (@PC Ax0)))) (or (or (@BetS Ax0 (@PB Ax0) (@PC Ax0) (@PA Ax0)) (or (@Logic.eq (@Point Ax0) (@PB Ax0) (@PC Ax0)) (@Logic.eq (@Point Ax0) (@PC Ax0) (@PA Ax0)))) (or (@BetS Ax0 (@PC Ax0) (@PA Ax0) (@PB Ax0)) (or (@Logic.eq (@Point Ax0) (@PC Ax0) (@PA Ax0)) (@Logic.eq (@Point Ax0) (@PA Ax0) (@PB Ax0)))))) *)
  intro;spliter.
  decompose [or] H;try
  solve [auto using  axiom_betweennesssymmetry].
Qed.

End Euclid_to_Tarski.


