proposition: Lemma t22_8__obtuse : forall A B C D R S, Saccheri A B C D -> Bet B C R -> Bet A D S -> D <> S -> Per A S R -> Lt R S A B -> Obtuse A B C.
proof: Proof. intros A B C D R S HSac HR HS HDS HPer Hlt. assert(Hdiff := sac_distincts A B C D HSac). spliter. assert(HI := l5_5_1 S R A B). destruct HI as [I []]; Le. assert_diffs. assert(HPar := sac__pars1423 A B C D HSac). assert(R <> I) by (intro; subst I; destruct Hlt; Cong). assert(R <> S) by (intro; apply HPar; exists R; subst; split; Col). assert(CongA A B C B C D) by (apply sac__conga; auto). destruct (t22_8_aux A B C D R S I) as [HCR [HSac1 [HSac2 [HOS HCop]]]]; [Out; Cong..|]. apply (lea_obtuse_obtuse _ _ _ B C D); [|apply conga__lea; CongA]. apply (obtuse_chara _ _ _ R); auto. assert(CongA A B I B I S) by (apply sac__conga; auto). assert(CongA D C I C I S) by (apply sac__conga; auto). assert_diffs. assert(HPar1 := sac__pars1234 A B I S HSac1). assert(HPar2 := sac__pars1423 D C I S HSac2). assert(HOS1 : OS C R S D). { apply one_side_symmetry, col_one_side with B; Col. apply par_strict_all_one_side with A; Par; Col. } assert(HNCol1 := one_side_not_col123 C R S D HOS1). assert(HNCol2 : ~ Col B C I) by (intro; apply HNCol1; ColR). assert(HTS : TS C R I D). { apply l9_2, (l9_8_2 _ _ S); Side. apply invert_two_sides, bet__ts; Col. } apply(sams_lta2_suma2__lta456 I C R _ _ _ D C I I B C _ _ _ A B I). - apply lta_left_comm, l11_41; Col. - assert(OS R S C B) by (apply out_one_side; Out; Col). apply (conga_preserves_lta S I C S I B); CongA. split. { exists C. split; CongA. apply os2__inangle; Side. apply one_side_transitivity with R. - apply par_strict_not_col_2 in HPar1. apply out_one_side; Out; Col. - apply invert_one_side, out_one_side; Out; Col. } intro Habs. apply conga_os__out in Habs; trivial. apply HNCol2; Col. - apply os_ts__sams; trivial. apply one_side_transitivity with S; Side. apply two_sides_not_col in HTS. apply out_one_side; Out; Col. - SumA. - exists A. repeat (split; CongA); [|Cop]. assert (OS B C A S) by (apply par_strict_all_one_side with D; Par; Col). apply l9_9, l9_2, (l9_8_2 _ _ S); Side. repeat split; Col. intro; apply (one_side_not_col124 B C A S); Col. exists R; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma