proposition: Lemma t22_8__acute : 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 A B R S -> Acute 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(HJ := Hlt). apply lt_right_comm in HJ. destruct HJ as [[J []] _]. assert_diffs. assert(J <> R) by (intro; subst J; destruct Hlt; Cong). assert(CongA A B C B C D) by (apply sac__conga; auto). destruct (t22_8_aux A B C D R S J) as [HCR [HSac1 [HSac2 [HOS HCop]]]]; [Out; Cong..|]. apply (acute_lea_acute _ _ _ B C D); Lea. apply (acute_chara _ _ _ R); auto. assert(CongA A B J B J S) by (apply sac__conga; auto). assert(CongA D C J C J S) by (apply sac__conga; auto). assert_diffs. assert(HPar1 := sac__pars1234 A B J S HSac1). assert(HPar2 := sac__pars1423 D C J S HSac2). assert(HNCol1 : ~ Col B J S) by (apply (par_strict_not_col_2 A), HPar1). assert(TS C J D R). { apply (l9_8_2 _ _ S). apply par_strict_not_col_2 in HPar2; apply invert_two_sides, bet__ts; Col. apply l12_6; Par. } assert (TS J B C S). { assert (HTS : TS J B R S) by (apply l9_2, bet__ts; Col). apply (l9_8_2 _ _ R); trivial. apply two_sides_not_col in HTS. apply invert_one_side, out_one_side; [Col|Out]. } assert (HNCol2 : ~ Col J B C) by (apply two_sides_not_col with S; auto). apply (sams_lta2_suma2__lta A B J J B C _ _ _ D C J J C R); [..|SumA]. - apply (conga_preserves_lta S J B S J C); CongA. split. apply inangle__lea; Side. intro Habs. apply HNCol2, out_col, (conga_os__out S); Side. - apply (conga_preserves_lta C B J J C R); CongA. apply l11_41; Col. - apply os_ts__sams; trivial. apply par_strict_all_one_side with S; Col. apply sac__pars1234, HSac2. - exists C. repeat (split; CongA); [|Cop]. assert(HPar3 := sac__pars1423 A B J S HSac1). apply l9_9, (l9_8_2 _ _ S); [|Side]. apply l9_2, (l9_8_2 _ _ R). apply l9_2, invert_two_sides, bet__ts; Col. apply out_one_side; [Col|Out]. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma