Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Axioms.parallel_postulates.
Require Export GeoCoq.Meta_theory.Parallel_postulates.proclus_SPP.
Require Export GeoCoq.Meta_theory.Parallel_postulates.SPP_tarski.
Require Export GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair.
Require Export GeoCoq.Meta_theory.Parallel_postulates.playfair_alternate_interior_angles.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section proclus_aristotle.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma proclus__aristotle : proclus_postulate -> aristotle_s_axiom.
Proof.
(* Goal: forall _ : @proclus_postulate Tn, @aristotle_s_axiom Tn *)
  intros proclus P Q A B C HNCol Hacute.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(HD0 := l10_15 B A B C).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  destruct HD0 as [D0 []]; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(HD := segment_construction B D0 P Q).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  destruct HD as [D []].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(HNCol1 : ~ Col B A D0) by (apply perp_not_col; auto).
(* Goal: @Cong Tn B D X Y *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(D<>B) by (intro;Between).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(~ Col D B A) by (intro; apply HNCol1; ColR).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(HY0 := l10_15 D B D A).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  destruct HY0 as [Y0 [HPerp HOS]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(Perp B A B D) by (apply (perp_col1 _ _ _ D0); Perp; Col).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(HPar : Par B A Y0 D).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
    {
(* Goal: @Par Tn B A Y0 D *)
    apply (l12_9 _ _ _ _ D B); Perp; Cop.
    }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(HY := proclus B A Y0 D B C).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  destruct HY as [Y []]; Col.
(* Goal: @Coplanar Tn B A D Y *)
(* Goal: not (@Col Tn B D Y) *)
  assert (Coplanar B A C D0) by Cop.
  assert (Coplanar A C B D)
    by (assert_diffs; assert_cols; apply col2_cop__cop with B D0; Col; Cop).
(* Goal: @Coplanar Tn Y0 D B C *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert (Coplanar D B A Y0) by Cop.
(* Goal: @Coplanar Tn Y0 D B C *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  CopR.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  apply (par_not_col_strict _ _ _ _ D) in HPar; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(~ Col Y B A) by (apply (par_not_col Y0 D); Col; Par).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  assert(HX := l8_18_existence A B Y).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  destruct HX as [X []]; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
  exists X.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y)))) *)
  exists Y.

(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(OS B A C D).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  { apply (one_side_transitivity _ _ _ D0); auto.
(* Goal: @OS Tn B A D0 D *)
    apply out_one_side; Col.
(* Goal: @Out Tn B D0 D *)
    apply bet_out; Between.
  }
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(Hlta : LtA A B C A B D).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  { destruct Hacute as [A' [B' [C' [HPer Hlta]]]].
(* Goal: @LtA Tn A B C A B D *)
    apply (conga_preserves_lta A B C A' B' C'); try (apply conga_refl); auto.
(* Goal: @CongA Tn A' B' C' A B D *)
    destruct Hlta.
(* Goal: @Cong Tn B D X Y *)
    assert_diffs.
(* Goal: @CongA Tn A' B' C' A B D *)
    apply l11_16; auto.
(* Goal: @Per Tn A B D *)
    apply perp_per_2; auto.
  }
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(HNCol2 : ~ Col B C D).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  { intro.
(* Goal: False *)
    elim(bet_dec C B D).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
    { intro.
(* Goal: False *)
      assert(~ OS B A C D); auto.
(* Goal: not (@OS Tn B A C D) *)
      apply l9_9.
(* Goal: and (@Col Tn B B A) (@Bet Tn C B D) *)
      repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T B A) (@Bet Tn C T D)) *)
      exists B.
(* Goal: and (@Col Tn B B A) (@Bet Tn C B D) *)
      repeat split; Col.
    }
(* Goal: not (@Cong Tn P Q X Y) *)
    intro.
(* Goal: False *)
    destruct Hlta as [_ HNConga].
(* Goal: False *)
    apply HNConga.
(* Goal: @CongA Tn A B C A B D *)
    apply (out_conga A B C A B C); try (apply out_trivial); CongA.
(* Goal: @Out Tn B C D *)
    apply not_bet_out; Col.
  }
(* Goal: @Cong Tn B D X Y *)
  assert_diffs.
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(Y<>D) by (intro; subst Y; Col).
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(OS B A C D).
(* Goal: @OS Tn B A C D *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
    apply (one_side_transitivity _ _ _ D0); auto; apply out_one_side; Col; apply bet_out; auto.
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(Par_strict B D X Y).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  { apply (par_not_col_strict _ _ _ _ Y); Col.
(* Goal: @Par Tn B D X Y *)
(* Goal: not (@Col Tn B D Y) *)
    apply (l12_9 _ _ _ _ B A); Perp; Cop.
(* Goal: @Coplanar Tn B A D Y *)
(* Goal: not (@Col Tn B D Y) *)
  assert (Coplanar B A C D0) by Cop.
  assert (Coplanar A C B D)
    by (assert_diffs; assert_cols; apply col2_cop__cop with B D0; Col; Cop).
(* Goal: @Coplanar Tn B A D Y *)
(* Goal: not (@Col Tn B D Y) *)
  apply coplanar_perm_12, col2_cop__cop with B C; Col; Cop.
(* Goal: not (@Col Tn B D Y) *)
    intro; assert(Col B C D); Col; ColR.
  }
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(InAngle C A B D) by (apply lea_in_angle; Lea; CongA; Side).
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(Out B C Y).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  { apply (col_one_side_out _ A); Col.
(* Goal: @OS Tn B A C Y *)
    apply (one_side_transitivity _ _ _ D); auto.
(* Goal: @OS Tn B A D Y *)
    apply l12_6.
(* Goal: @Par_strict Tn B A D Y *)
    apply (par_strict_col_par_strict _ _ _ Y0); Par; Col.
  }

(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(Out B A X).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  { apply (col_one_side_out _ D); Col.
(* Goal: @OS Tn B D A X *)
    apply one_side_symmetry.
(* Goal: @OS Tn B D X A *)
    apply (one_side_transitivity _ _ _ Y).
(* Goal: @OS Tn B D X Y *)
(* Goal: @OS Tn B D Y A *)
    apply l12_6; auto.
(* Goal: @OS Tn B D Y A *)
    apply (one_side_transitivity _ _ _ C).
(* Goal: @OS Tn B D Y C *)
(* Goal: @OS Tn B D C A *)
    apply out_one_side; try (apply l6_6); Col.
(* Goal: @OS Tn B D C A *)
    apply invert_one_side.
(* Goal: @OS Tn D B C A *)
    apply in_angle_one_side; try (apply l11_24); Col.
  }

(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(Per B X Y).
(* Goal: @Cong Tn B D X Y *)
(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  { assert (~ Col B D X) by (apply (par_strict_not_col_1 _ _ _ Y); auto).
(* Goal: @Cong Tn B D X Y *)
    assert_diffs.
(* Goal: @Per Tn B X Y *)
    apply perp_per_1; auto.
(* Goal: @Perp Tn X B Y X *)
    apply perp_left_comm.
(* Goal: @Perp Tn B X Y X *)
    apply (perp_col _ A); Col; Perp.
  }

(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  assert(Cong B D X Y).
(* Goal: @Cong Tn B D X Y *)
  { assert_diffs.
(* Goal: @Cong Tn B D X Y *)
    assert(HAAS := l11_50_2 B Y D Y B X).
(* Goal: @Cong Tn B D X Y *)
    destruct HAAS; Cong.
(* Goal: not (@Col Tn B Y D) *)
(* Goal: @CongA Tn Y D B B X Y *)
(* Goal: @CongA Tn B Y D Y B X *)
      apply not_col_permutation_5; apply (par_strict_not_col_4 _ _ X); auto.
(* Goal: @CongA Tn Y D B B X Y *)
(* Goal: @CongA Tn B Y D Y B X *)
      apply l11_16; Perp; apply perp_per_2; auto; apply (perp_col _ Y0); Col; Perp.
(* Goal: @CongA Tn B Y D Y B X *)
    apply conga_comm.

(* proclus -> alternate_interior *)
(* Goal: @CongA Tn D Y B X B Y *)
apply proclus_s_postulate_implies_strong_parallel_postulate in proclus.
(* Goal: @CongA Tn D Y B X B Y *)
apply strong_parallel_postulate_implies_tarski_s_euclid in proclus.
(* Goal: @CongA Tn D Y B X B Y *)
apply tarski_s_euclid_implies_playfair in proclus.
(* Goal: @CongA Tn D Y B X B Y *)
apply playfair__alternate_interior in proclus.
(* Goal: @CongA Tn D Y B X B Y *)
rename proclus into aia.

(* Goal: @CongA Tn D Y B X B Y *)
    apply aia.
    - apply l9_2.
(* Goal: @TS Tn Y B X D *)
      apply (l9_8_2 _ _ A).
(* Goal: @TS Tn Y B A D *)
(* Goal: @OS Tn Y B A X *)
      apply (col_preserves_two_sides C B); Col; apply in_angle_two_sides; Col.
(* Goal: @OS Tn B A D0 D *)
      apply invert_one_side; apply out_one_side; Col.

    - apply par_left_comm.
(* Goal: @Par Tn D Y B X *)
      apply (par_col_par _ _ _ A); Col.
(* Goal: @Par Tn D Y B A *)
      apply (par_col_par_2 _ Y0); Col.
(* Goal: @Par Tn D Y0 B A *)
      apply par_strict_par; Par.
   }

(* Goal: and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))) *)
  repeat (split; auto).
  - apply (l5_6 P Q B D); Cong.
(* Goal: @Le Tn P Q B D *)
    apply le_right_comm.
(* Goal: @Le Tn P Q D B *)
    exists D0.
(* Goal: and (@Bet Tn D D0 B) (@Cong Tn P Q D D0) *)
    split; Between; Cong.

(* Goal: not (@Cong Tn P Q X Y) *)
  - intro.
(* Goal: False *)
    assert(D0=B); auto.
(* Goal: @eq (@Tpoint Tn) D0 B *)
    apply (between_cong D B D0); Between.
(* Goal: @Cong Tn D D0 D B *)
    apply (cong_transitivity _ _ P Q).
(* Goal: @Cong Tn D D0 P Q *)
(* Goal: @Cong Tn P Q D B *)
    Cong.
(* Goal: @Cong Tn D D0 P Q *)
(* Goal: @Cong Tn P Q D B *)
    apply (cong_transitivity _ _ X Y); Cong.
Qed.

End proclus_aristotle.