proposition: 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: Proof. intros A B C D E F HNCol HCongaB HCongaC HCongaA Hlea Hlt. assert_diffs. destruct (segment_construction_3 A B D E) as [G []]; auto. rename H into HFD. destruct (segment_construction_3 A C D F) as [H []]; auto. apply (cong2_lt__lt _ _ _ _ A G A B) in Hlt; Cong. assert(Bet A G B) by (apply (l6_13_1); Le; apply l6_6; auto). assert(B <> G) by (intro; subst; destruct Hlt; Cong). assert(HCongaA' : CongA C A B H A G) by (apply out2__conga; apply l6_6; auto). destruct(l11_49 F D E H A G) as [_ [HConga1 HConga2]]; Cong. apply (conga_trans _ _ _ C A B); CongA. apply (conga_trans _ _ _ _ _ _ A G H) in HCongaB; auto. apply (conga_trans _ _ _ _ _ _ G H A) in HCongaC; CongA. clear dependent D; clear dependent E; clear dependent F. rename HCongaA' into HCongaA. assert(HNCol1 : ~ Col A G H) by (apply (ncol_conga_ncol A B C); auto). assert(HNCol2 : ~ Col B G H) by (intro; apply HNCol1; ColR). assert(Par_strict G H B C). { apply (par_not_col_strict _ _ _ _ B); Col. apply par_symmetry. apply (l12_22_b _ _ _ _ A); CongA. apply out_one_side; auto. } assert(HNCol3 : ~ Col G H C) by (apply (par_strict_not_col_4 _ _ B); auto). assert(HNCol4 : ~ Col B C G) by (apply (par_strict_not_col_3 _ H); auto). assert(HNCol5 : ~ Col H B C) by (apply (par_strict_not_col_2 G); auto). assert_diffs. assert(Out C H A). { apply (col_one_side_out _ B); Col. apply invert_one_side. apply (one_side_transitivity _ _ _ G). apply l12_6; Par. apply out_one_side; Col; apply bet_out; Between. } assert(Bet A H C) by (apply out2__bet; apply l6_6; auto). assert(SAMS B G H H C B). { apply (sams_chara _ _ _ _ _ _ A); Between. apply (l11_30 B C A A B C); auto; apply conga_right_comm; auto. apply out2__conga; [apply out_trivial|]; auto. } assert(CongA A G H G B C). apply (l11_10 A G H A B C); try (apply out_trivial); CongA; apply bet_out; Between. assert(CongA G H A B C H). apply (l11_10 G H A B C A); try (apply out_trivial); CongA. assert(SAMS B G H C B G) by (apply (conga2_sams__sams B G H H G A); CongA; SumA). assert(SAMS C H G B C H) by (apply (conga2_sams__sams C H G G H A); CongA; SumA). destruct(ex_suma B C G C G B) as [I [J [K]]]; auto. destruct(ex_suma H C G C G H) as [L [M [N]]]; auto. suma.assert_diffs. destruct(ex_suma I J K G B C) as [O [P [Q]]]; auto. destruct(ex_suma L M N G H C) as [R [S [T]]]; auto. destruct(ex_suma I J K L M N) as [U [V [W]]]; auto. suma.assert_diffs. assert(HInter : SAMS I J K L M N /\ SumA H G B B C H U V W). { assert(TS G C B H). { apply invert_two_sides, l9_31; Side. apply (col_one_side _ A); Col. apply invert_one_side; apply out_one_side; try (apply l6_6); Col. } assert(SAMS H G B B C G). { apply (sams_lea2__sams _ _ _ _ _ _ H G B B C H); try (apply lea_refl); SumA. apply inangle__lea. apply os_ts__inangle; Side. } destruct(ex_suma B C G H G B) as [X [Y [Z]]]; auto. assert(SumA B G C C G H H G B) by SumA. assert(SAMS B G C C G H). { apply os_ts__sams; trivial. apply (col_one_side _ A); Col. apply invert_one_side, out_one_side; Col. } assert(SAMS I J K C G H) by (apply (sams_assoc B C G C G B _ _ _ _ _ _ H G B); SumA). 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). assert(SAMS B C G H C G) by (apply sams_right_comm, os_ts__sams; Side). assert(SumA B C G H C G H C B) by SumA. split. - assert(SAMS X Y Z H C G) by (apply (sams_assoc H G B B C G _ _ _ _ _ _ H C B); SumA). 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). apply (suma_assoc _ _ _ B C G H C G _ _ _ X Y Z); SumA. } destruct HInter. elim(saccheri_s_three_hypotheses). - intro aah. exfalso. apply(nlta U V W). apply (sams_lta2_suma2__lta I J K L M N _ _ _ H G B B C H); SumA. { destruct (t22_14__sams_nbet aah C G B I J K O P Q) as [HIsi HNBet]; Col. apply (sams_lea_lta789_suma2__lta123 _ _ _ G B C O P Q _ _ _ G B C A G B); Lea. split; Lea; intro; apply HNBet; apply (bet_conga__bet A G B); CongA. apply (conga3_suma__suma B G H H G A A G B); CongA; SumA. } destruct (t22_14__sams_nbet aah C G H L M N R S T) as [HIsi HNBet]; Col. apply (sams_lea_lta789_suma2__lta123 _ _ _ G H C R S T _ _ _ G H C A H C); Lea. split; Lea; intro; apply HNBet; apply (bet_conga__bet A H C); CongA. apply (conga3_suma__suma A H G G H C A H C); CongA; SumA. - intro HUn. destruct HUn as [|oah]; auto. exfalso. apply(nlta 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. { apply (t22_14__nsams oah C G B I J K); Col. apply (sams_lea2__sams _ _ _ _ _ _ H G B G B C); Lea; SumA. } apply (t22_14__nsams oah C G H L M N); Col. apply (sams_lea2__sams _ _ _ _ _ _ B C H G H C); Lea; SumA. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch12_parallel