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

Section similar_rah.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(**
This is an adaptation of the proof of Martin's Theorem 23.6.
It is more complicated because Martin use the properties of the deflect of a triangle,
which are difficult to handle in our formalization.
*)

Lemma similar__rah_aux : forall A B C D E F,
  ~ Col A B C -> CongA A B C D E F -> CongA B C A E F D -> CongA C A B F D E ->
  LeA B C A A B C -> Lt D E A B -> postulate_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @CongA Tn A B C D E F) (_ : @CongA Tn B C A E F D) (_ : @CongA Tn C A B F D E) (_ : @LeA Tn B C A A B C) (_ : @Lt Tn D E A B), @postulate_of_right_saccheri_quadrilaterals Tn *)
  intros A B C D E F HNCol HCongaB HCongaC HCongaA Hlea Hlt.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert_diffs.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct (segment_construction_3 A B D E) as [G []]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  rename H into HFD.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct (segment_construction_3 A C D F) as [H []]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  apply (cong2_lt__lt _ _ _ _ A G A B) in Hlt; Cong.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(Bet A G B) by (apply (l6_13_1); Le; apply l6_6; auto).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(B <> G) by (intro; subst; destruct Hlt; Cong).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(HCongaA' : CongA C A B H A G) by (apply (out_conga C A B C A B); try (apply out_trivial); CongA).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct(l11_49 F D E H A G) as [_ [HConga1 HConga2]]; Cong.
(* Goal: @CongA Tn F D E H A G *)
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (conga_trans _ _ _ C A B); CongA.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  apply (conga_trans _ _ _ _ _ _ A G H) in HCongaB; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  apply (conga_trans _ _ _ _ _ _ G H A) in HCongaC; CongA.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  clear dependent D; clear dependent E; clear dependent F.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  rename HCongaA' into HCongaA.

(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(HNCol1 : ~ Col A G H) by (apply (ncol_conga_ncol A B C); auto).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(HNCol2 : ~ Col B G H) by (intro; apply HNCol1; ColR).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(Par_strict G H B C).
(* Goal: False *)
(* Goal: False *)
  { apply (par_not_col_strict _ _ _ _ B); Col.
(* Goal: @Par Tn G H B C *)
    apply par_symmetry.
(* Goal: @Par Tn B C G H *)
    apply (l12_22_b _ _ _ _ A); CongA.
(* Goal: @OS Tn A B C H *)
    apply out_one_side; auto.
  }
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(HNCol3 : ~ Col G H C) by (apply (par_strict_not_col_4 _ _ B); auto).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(HNCol4 : ~ Col B C G) by (apply (par_strict_not_col_3 _ H); auto).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(HNCol5 : ~ Col H B C) by (apply (par_strict_not_col_2 G); auto).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert_diffs.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(Out C H A).
(* Goal: False *)
(* Goal: False *)
  { apply (col_one_side_out _ B); Col.
(* Goal: @OS Tn C B H A *)
    apply invert_one_side.
(* Goal: @OS Tn B C H A *)
    apply (one_side_transitivity _ _ _ G).
(* Goal: @OS Tn B C H G *)
(* Goal: @OS Tn B C G A *)
      apply l12_6; Par.
(* Goal: @OS Tn B C G A *)
      apply out_one_side; Col; apply bet_out; Between.
  }
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(Bet A H C) by (apply out2__bet; apply l6_6; auto).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(SAMS B G H H C B).
(* Goal: False *)
(* Goal: False *)
  { apply (sams_chara _ _ _ _ _ _ A); Between.
(* Goal: @LeA Tn H C B H G A *)
    apply (l11_30 B C A A B C); auto; apply conga_right_comm; auto.
(* Goal: @CongA Tn B C A B C H *)
    apply (out_conga B C H B C H); try (apply out_trivial); CongA.
  }
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(CongA A G H G B C).
(* Goal: @CongA Tn A G H G B C *)
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (out_conga A G H A B C); try (apply out_trivial); CongA; apply l6_6; apply bet_out; Between.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(CongA G H A B C H).
(* Goal: @CongA Tn G H A B C H *)
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (out_conga G H A B C A); try (apply out_trivial); CongA; apply l6_6; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(TS G H A B) by (repeat split; auto; exists G; Col).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(TS G H A C) by (repeat split; Col; exists H; Col).
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(TS C G B H).
(* Goal: False *)
(* Goal: False *)
  { apply l9_31; eauto with side.
(* Goal: @OS Tn B G C H *)
    apply (col_one_side _ A); Col.
(* Goal: @OS Tn C A G B *)
    apply invert_one_side; apply out_one_side; try (apply l6_6); Col.
  }
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(SAMS B G H C B G).
(* Goal: False *)
(* Goal: False *)
  { apply (conga2_sams__sams B G H H G A); CongA.
(* Goal: @SAMS Tn B G C C G H *)
    repeat split; auto.
(* Goal: or (@Out Tn G H A) (not (@Bet Tn B G H)) *)
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn H G J H G A) (and (not (@OS Tn G H B J)) (and (not (@TS Tn B G H J)) (@Coplanar Tn B G H J)))) *)
    right; intro; Col.
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn G H J G H A) (and (not (@OS Tn H G C J)) (and (not (@TS Tn C H G J)) (@Coplanar Tn C H G J)))) *)
    exists A; split; CongA.
(* Goal: and (not (@OS Tn G C B H)) (and (not (@TS Tn B G C H)) (@Coplanar Tn B G C H)) *)
    split; Side.
(* Goal: and (not (@TS Tn B G C H)) (@Coplanar Tn B G C H) *)
    split; Cop.
(* Goal: not (@TS Tn C H G A) *)
    intro Hts.
(* Goal: False *)
    destruct Hts as [_ []]; Col.
  }
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(SAMS C H G B C H).
(* Goal: False *)
(* Goal: False *)
  { apply (conga2_sams__sams C H G G H A); CongA.
(* Goal: @SAMS Tn B G C C G H *)
    repeat split; auto.
(* Goal: or (@Out Tn H G A) (not (@Bet Tn C H G)) *)
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn G H J G H A) (and (not (@OS Tn H G C J)) (and (not (@TS Tn C H G J)) (@Coplanar Tn C H G J)))) *)
    right; intro; apply HNCol3; Col.
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn G H J G H A) (and (not (@OS Tn H G C J)) (and (not (@TS Tn C H G J)) (@Coplanar Tn C H G J)))) *)
    exists A; split; CongA.
(* Goal: and (not (@OS Tn G C B H)) (and (not (@TS Tn B G C H)) (@Coplanar Tn B G C H)) *)
    split; Side.
(* Goal: and (not (@TS Tn B G C H)) (@Coplanar Tn B G C H) *)
    split; Cop.
(* Goal: not (@TS Tn C H G A) *)
    intro Hts.
(* Goal: False *)
    destruct Hts as [_ []]; Col.
  }
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct(ex_suma B C G C G B) as [I [J [K]]]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct(ex_suma H C G C G H) as [L [M [N]]]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  suma.assert_diffs.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct(ex_suma I J K G B C) as [O [P [Q]]]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct(ex_suma L M N G H C) as [R [S [T]]]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct(ex_suma I J K L M N) as [U [V [W]]]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  suma.assert_diffs.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert(HInter : SAMS I J K L M N /\ SumA H G B B C H U V W).
(* Goal: False *)
(* Goal: False *)
  { assert(SAMS H G B B C G).
(* Goal: False *)
(* Goal: False *)
    { apply (sams_lea2__sams _ _ _ _ _ _ H G B B C H); try (apply lea_refl); SumA.
(* Goal: @LeA Tn B C G B C H *)
      exists G; split; CongA.
(* Goal: @InAngle Tn G B C H *)
      apply os_ts__inangle; SumA; eauto with side.
    }
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
    destruct(ex_suma B C G H G B) as [X [Y [Z]]]; auto.
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
    assert(SumA B G C C G H H G B) by (exists H; repeat (split; CongA); Side; Cop).
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
    assert(SAMS B G C C G H).
(* Goal: False *)
(* Goal: False *)
    { repeat split; auto.
(* Goal: or (@Out Tn G C H) (not (@Bet Tn B G C)) *)
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn C G J C G H) (and (not (@OS Tn G C B J)) (and (not (@TS Tn B G C J)) (@Coplanar Tn B G C J)))) *)
        right; intro; apply HNCol4; Col.
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn C G J C G H) (and (not (@OS Tn G C B J)) (and (not (@TS Tn B G C J)) (@Coplanar Tn B G C J)))) *)
      exists H; split; CongA.
(* Goal: and (not (@OS Tn G C B H)) (and (not (@TS Tn B G C H)) (@Coplanar Tn B G C H)) *)
      split; Side.
(* Goal: and (not (@TS Tn B G C H)) (@Coplanar Tn B G C H) *)
      split; Cop.
(* Goal: not (@TS Tn B G C H) *)
      apply l9_9_bis.
(* Goal: @OS Tn B G C H *)
      apply (col_one_side _ A); Col.
(* Goal: @OS Tn B A C H *)
      apply invert_one_side, out_one_side; Col.
    }
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
    assert(SAMS I J K C G H) by (apply (sams_assoc B C G C G B _ _ _ _ _ _ H G B); SumA).
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
    assert(SumA I J K C G H X Y Z) by (apply (suma_assoc B C G C G B _ _ _ _ _ _ _ _ _ H G B); SumA).
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
    assert(SAMS B C G H C G).
(* Goal: @SAMS Tn B C G H C G *)
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
      repeat split; auto; [right; intro; Col|exists H; split; CongA; repeat split; Side; Cop].
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
    assert(SumA B C G H C G H C B) by (exists H; repeat (split; CongA); Side; Cop).
(* Goal: and (@SAMS Tn I J K L M N) (@SumA Tn H G B B C H U V W) *)
    split.
    - assert(SAMS X Y Z H C G) by (apply (sams_assoc H G B B C G _ _ _ _ _ _ H C B); SumA).
(* Goal: @SAMS Tn I J K L M N *)
      apply (sams_assoc _ _ _ C G H H C G X Y Z); SumA.
    - assert(SumA X Y Z H C G U V W) by (apply (suma_assoc I J K C G H _ _ _ _ _ _ _ _ _ L M N); SumA).
(* Goal: @SumA Tn H G B B C H U V W *)
      apply (suma_assoc _ _ _ B C G H C G _ _ _ X Y Z); SumA.
  }
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct HInter.

(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  elim(saccheri_s_three_hypotheses).
  - intro aah.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    exfalso.
(* Goal: False *)
    apply(nlta U V W).
(* Goal: @LtA Tn U V W U V W *)
    apply (sams_lta2_suma2__lta I J K L M N _ _ _ H G B B C H); SumA.
(* Goal: False *)
(* Goal: False *)
    { destruct (t22_14__sams_nbet aah C G B I J K O P Q) as [HIsi HNBet]; Col.
(* Goal: @LtA Tn I J K H G B *)
      apply (sams_lea_lta789_suma2__lta123 _ _ _ G B C O P Q _ _ _ G B C A G B); Lea.
(* Goal: @LtA Tn O P Q A G B *)
(* Goal: @SumA Tn H G B G B C A G B *)
        split; eauto with lea; intro; apply HNBet; apply (bet_conga__bet A G B); CongA.
(* Goal: @SumA Tn H G B G B C A G B *)
        apply (conga3_suma__suma B G H H G A A G B); CongA; exists A; repeat (split; CongA); Side; Cop.
    }
(* Goal: @LtA Tn L M N B C H *)
    destruct (t22_14__sams_nbet aah C G H L M N R S T) as [HIsi HNBet]; Col.
(* Goal: @LtA Tn L M N B C H *)
    apply (sams_lea_lta789_suma2__lta123 _ _ _ G H C R S T _ _ _ G H C A H C); Lea.
(* Goal: @LtA Tn R S T A H C *)
(* Goal: @SumA Tn B C H G H C A H C *)
      split; eauto with lea; intro; apply HNBet; apply (bet_conga__bet A H C); CongA.
(* Goal: @SumA Tn B C H G H C A H C *)
      apply (conga3_suma__suma A H G G H C A H C); CongA; exists C; repeat (split; CongA); Side; Cop.

  - intro HUn.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    destruct HUn as [|oah]; auto.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    exfalso.
(* Goal: False *)
    apply(nlta U V W).
(* Goal: @LtA Tn U V W U V W *)
    apply (sams_lta2_suma2__lta H G B B C H _ _ _ I J K L M N); SumA; apply nlea__lta; auto; intro.
(* Goal: False *)
(* Goal: False *)
    { apply (t22_14__nsams oah C G B I J K); Col.
(* Goal: @SAMS Tn I J K G B C *)
      apply (sams_lea2__sams _ _ _ _ _ _ H G B G B C); Lea; SumA.
    }
(* Goal: False *)
    apply (t22_14__nsams oah C G H L M N); Col.
(* Goal: @SAMS Tn L M N G H C *)
    apply (sams_lea2__sams _ _ _ _ _ _ B C H G H C); Lea; SumA.
Qed.

Lemma similar__rah : postulate_of_existence_of_similar_triangles -> postulate_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : @postulate_of_existence_of_similar_triangles Tn, @postulate_of_right_saccheri_quadrilaterals Tn *)
  intro similar.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct similar as [A [B [C [D [E [F]]]]]].
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  spliter.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  assert_diffs.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  elim (lea_total B C A A B C); auto; intro; [elim (le_cases D E A B)|elim (le_cases D F A C)].
  - intro.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (similar__rah_aux A B C D E F); auto.
(* Goal: @Lt Tn D E A B *)
    split; Cong.

  - intro.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (similar__rah_aux D E F A B C); CongA.
(* Goal: not (@Col Tn D E F) *)
(* Goal: @LeA Tn E F D D E F *)
(* Goal: @Lt Tn A B D E *)
      apply (ncol_conga_ncol A B C); auto.
(* Goal: @LeA Tn E F D D E F *)
(* Goal: @Lt Tn A B D E *)
      apply (l11_30 B C A A B C); auto.
(* Goal: @Lt Tn A B D E *)
      split; auto.

  - intro.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (similar__rah_aux A C B D F E); Col; CongA.
(* Goal: @LeA Tn C B A A C B *)
(* Goal: @Lt Tn D F A C *)
      apply lea_comm; trivial.
(* Goal: @Lt Tn A C D F *)
    split; auto; intro; destruct(l11_50_1 A C B D F E); Col; CongA; Cong.

  - intro.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
    apply (similar__rah_aux D F E A C B); CongA.
(* Goal: not (@Col Tn D F E) *)
(* Goal: @LeA Tn F E D D F E *)
(* Goal: @Lt Tn A C D F *)
      apply (ncol_conga_ncol A C B); Col; CongA.
(* Goal: @LeA Tn F E D D F E *)
(* Goal: @Lt Tn A C D F *)
      apply (l11_30 A B C B C A); CongA.
(* Goal: @Lt Tn A C D F *)
      split; auto; intro; destruct(l11_50_1 A C B D F E); Col; CongA; Cong.
Qed.

End similar_rah.