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

Section rah_similar.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma rah__similar : postulate_of_right_saccheri_quadrilaterals -> postulate_of_existence_of_similar_triangles.
Proof.
(* Goal: forall _ : @postulate_of_right_saccheri_quadrilaterals Tn, @postulate_of_existence_of_similar_triangles Tn *)
  intro rah.
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  destruct lower_dim_ex as [A [B0 [C]]].
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  assert(~ Col A B0 C) by (unfold Col; assumption).
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  destruct (l10_15 C A C B0) as [B []]; Col.
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  assert(HNCol1 : ~ Col C A B) by (apply (one_side_not_col123 _ _ _ B0); Side).
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  assert(Per A C B) by Perp.
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  destruct (symmetric_point_construction A B) as [B'].
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert_diffs.
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  assert(HNCol2 : ~ Col A C B') by (intro; apply HNCol1; ColR).
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  assert(HNCol3 : ~ Col B B' C) by (intro; apply HNCol2; ColR).
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  destruct (l8_18_existence A C B') as [C' []]; auto.
(* Goal: @postulate_of_existence_of_similar_triangles Tn *)
  exists A; exists B; exists C; exists A; exists B'; exists C'.
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert(Par_strict B C B' C').
(* Goal: @Par_strict Tn B C B' C' *)
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
    apply (par_not_col_strict _ _ _ _ B'); Col; apply (l12_9 _ _ _ _ A C); Perp; Cop.
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert(HNCol4 : ~ Col B C C') by (apply (par_strict_not_col_4 _ _ B'); auto).
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert_diffs.
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert(Bet A C C').
(* Goal: and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')) *)
  { apply (col_two_sides_bet _ B); Col.
(* Goal: @TS Tn C B A C' *)
    apply l9_2.
(* Goal: @TS Tn C B C' A *)
    apply (l9_8_2 _ _ B').
(* Goal: @TS Tn C B B' A *)
(* Goal: @OS Tn C B B' C' *)
      repeat split; Col; exists B; split; Col; Between.
(* Goal: @OS Tn C B B' C' *)
      apply l12_6; Par.
  }
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert(A <> C') by (intro; treat_equalities; auto).
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert(Per B' C' A) by (apply perp_per_1; auto; apply (perp_col1 _ _ _ C); Col; Perp).
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert(CongA B C A B' C' A) by (apply l11_16; Perp).
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  assert(CongA C A B C' A B').
(* Goal: @CongA Tn C A B C' A B' *)
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
    apply (out_conga C A B C A B); try (apply out_trivial); CongA; apply bet_out; Between.
(* Goal: and (not (@Col Tn A B C)) (and (not (@Cong Tn A B A B')) (and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')))) *)
  split; Col; split.

(* Goal: and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')) *)
    {
(* Goal: not (@Cong Tn A B A B') *)
    intro.
(* Goal: False *)
    absurd(B = B'); auto.
(* Goal: @eq (@Tpoint Tn) B B' *)
    apply (between_cong A); Between.
    }

(* Goal: and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')) *)
    {
(* Goal: and (@CongA Tn A B C A B' C') (and (@CongA Tn B C A B' C' A) (@CongA Tn C A B C' A B')) *)
    split; [|repeat (split; auto)].
(* Goal: @CongA Tn A B C A B' C' *)
    apply (sams2_suma2__conga456 C A B _ _ _ _ _ _ B C A).
(* Goal: @SAMS Tn C A B A B C *)
(* Goal: @SAMS Tn C A B A B' C' *)
(* Goal: @SumA Tn C A B A B C B C A *)
(* Goal: @SumA Tn C A B A B' C' B C A *)
    SumA.
(* Goal: @SAMS Tn C A B A B C *)
(* Goal: @SAMS Tn C A B A B' C' *)
(* Goal: @SumA Tn C A B A B C B C A *)
(* Goal: @SumA Tn C A B A B' C' B C A *)
    apply (conga2_sams__sams C' A B' A B' C'); CongA; SumA.
(* Goal: @SumA Tn C A B A B C B C A *)
(* Goal: @SumA Tn C A B A B' C' B C A *)
    apply t22_12__rah; Perp.
(* Goal: @SumA Tn C A B A B' C' B C A *)
    apply (conga3_suma__suma C' A B' A B' C' B' C' A); CongA; apply t22_12__rah; auto.
    }
Qed.

End rah_similar.