Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.
Require Import GeoCoq.Tarski_dev.Annexes.perp_bisect.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section existential_playfair_rah.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma existential_playfair__rah :
  existential_playfair_s_postulate ->
  postulate_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : @existential_playfair_s_postulate Tn, @postulate_of_right_saccheri_quadrilaterals Tn *)
intro HP; destruct HP as [A1 [A2 [P [HNC1 HP]]]].
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
destruct (l8_18_existence A1 A2 P) as [Q [HCcol1 HPerp1]]; Col.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
assert (HA3 : exists A3, Col A1 A2 A3 /\ A3 <> Q).
(* Goal: @Lambert Tn P Q S R *)
{
(* Goal: @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (not (@eq (@Tpoint Tn) A3 Q))) *)
  destruct (eq_dec_points A1 Q).
(* Goal: @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (not (@eq (@Tpoint Tn) A3 Q))) *)
(* Goal: @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (not (@eq (@Tpoint Tn) A3 Q))) *)
    subst; exists A2; assert_diffs; split; Col.
(* Goal: @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (not (@eq (@Tpoint Tn) A3 Q))) *)
    exists A1; split; Col.
}
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
destruct HA3 as [A3 []].
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
destruct (ex_perp_cop P Q P A3) as [R [HPerp2 HCop]].
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert_diffs; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
assert (HPar1 : Par A1 A2 P R).
(* Goal: @Lambert Tn P Q S R *)
{
(* Goal: @Par Tn A1 A2 P R' *)
  assert_diffs.
(* Goal: @Par Tn A1 A2 P R *)
  apply l12_9 with P Q; Perp.
(* Goal: @Coplanar Tn P Q A2 P *)
(* Goal: @Coplanar Tn P Q A2 R *)
    Cop.
(* Goal: @Coplanar Tn P Q A2 R *)
    apply coplanar_perm_3, col_cop__cop with A3; Cop; ColR.
(* Goal: @Coplanar Tn P Q A2 P *)
(* Goal: @Coplanar Tn P Q A2 R *)
    Cop.
(* Goal: @Coplanar Tn P Q A2 R *)
    apply coplanar_perm_3, col_cop__cop with A3; Cop; ColR.
}
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
assert (HCop1 : Coplanar A1 A2 P R) by (apply par__coplanar, HPar1).
assert (HNC2 : Par_strict A1 A2 P R)
  by (apply par_not_col_strict with P; Col).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
apply par_strict_not_col_4 in HNC2.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
destruct (l8_18_existence A1 A2 R) as [S [HCcol2 HPerp3]]; Col.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
assert (HPar2 : Par P Q R S) by (apply l12_9 with A1 A2; Perp; Cop).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
assert (HNC3 : ~ Col P Q R) by (apply perp_not_col; Perp).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
assert (HNC4 : Par_strict P Q R S) by (apply par_not_col_strict with R; Col).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
apply par_strict_not_col_3 in HNC4.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
destruct (l8_18_existence R S P) as [R' [HCcol3 HPerp4]]; Col.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
assert (HPar3 : Par A1 A2 P R').
(* Goal: @Lambert Tn P Q S R *)
{
(* Goal: @Par Tn A1 A2 P R' *)
  assert_diffs.
(* Goal: @Par Tn A1 A2 P R' *)
  apply l12_9 with R S; Perp.
(* Goal: @Coplanar Tn P Q A2 P *)
(* Goal: @Coplanar Tn P Q A2 R *)
    apply coplanar_perm_5, col_cop__cop with A2; Col; Cop.
(* Goal: @Coplanar Tn R S A2 R' *)
    exists R'; left; split; Col.
(* Goal: @Coplanar Tn P Q A2 P *)
(* Goal: @Coplanar Tn P Q A2 R *)
    apply coplanar_perm_5, col_cop__cop with A1; Col; Cop.
(* Goal: @Coplanar Tn R S A2 R' *)
    exists R'; left; split; Col.
}
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
destruct (HP P R P R') as [_ HCol4]; Col.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
assert (R = R') by (apply l6_21 with P R S R; assert_diffs; Col).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
treat_equalities; rewrite <- (lam_per__rah P Q S R).

(* Goal: @Lambert Tn P Q S R *)
  {
(* Goal: @Per Tn Q S R *)
  apply perp_in_per_1 with S S; apply l8_14_2_1b_bis; Col.
(* Goal: @Perp Tn Q S R S *)
  apply perp_sym; apply perp_col0 with A1 A2; Col.
(* Goal: @Lambert Tn P Q S R *)
  assert (HPs : Par_strict P Q R S) by (apply par_not_col_strict with R; Col).
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  apply par_strict_not_col_2 in HPs; assert_diffs; auto.
  }

(* Goal: @Lambert Tn P Q S R *)
  {
(* Goal: @Lambert Tn P Q S R *)
  assert (HPs : Par_strict P Q R S) by (apply par_not_col_strict with R; Col).
(* Goal: @Lambert Tn P Q S R *)
  apply par_strict_not_col_2 in HPs.
(* Goal: @Lambert Tn P Q S R *)
  repeat try (split; [intro; treat_equalities; assert_diffs; intuition|]).
(* Goal: and (@Per Tn Q P R) (and (@Per Tn P R S) (and (@Per Tn P Q S) (@Coplanar Tn P Q S R))) *)
  apply par__coplanar in HPar2.
(* Goal: @Coplanar Tn P Q A2 P *)
(* Goal: @Coplanar Tn P Q A2 R *)
  repeat split; Cop.
  - apply perp_in_per_1 with P P; apply l8_14_2_1b_bis; Col; Perp.
  - apply perp_in_per_1 with R R; apply l8_14_2_1b_bis; Col; Perp.
  - apply perp_in_per_1 with Q Q; apply l8_14_2_1b_bis; Col.
(* Goal: @Perp Tn P Q S Q *)
    apply perp_col0 with A1 A2; assert_diffs; Col.
  }
Qed.

End existential_playfair_rah.