proposition: Lemma bet_obtuse__acute : forall A B C A', Bet A B A' -> A' <> B -> Obtuse A B C -> Acute A' B C.
proof: Proof. intros A B C A' HBet HA'B Hobtuse. assert(Hd := obtuse_distincts A B C Hobtuse). spliter. elim(col_dec A B C). { intro. elim(bet_dec A B C). - intro. apply out__acute. apply (l6_2 _ _ A); Between. - intro. exfalso. apply (nlta A B C). apply acute_obtuse__lta; auto. apply out__acute. apply not_bet_out; auto. } intro HNCol1. assert(HD := l10_15 A B B C). destruct HD as [D []]; Col. assert_diffs. assert(HNCol2 : ~ Col C B D). { intro. apply (nlta A B C). apply obtuse_per__lta; auto. apply (per_col _ _ D); Perp; Col. } assert(OS B A' C D) by (apply (col_one_side _ A); Side; Col). assert(~ Col A B D) by (apply per_not_col; Perp). exists A'. exists B. exists D. split. apply (l8_3 A); Perp; Col. split. - exists C. split; try (apply conga_refl); auto. apply os2__inangle; Side. exists A. split. { repeat split; auto. apply (one_side_not_col123 _ _ _ C); Side. exists B; split; [Col|Between]. } apply invert_two_sides. apply in_angle_two_sides; Col. apply l11_24. apply lea_in_angle; try (apply conga_refl); auto. apply lta__lea. apply obtuse_per__lta; Perp. - intro Habs. assert (Out B C D) by (apply (conga_os__out A'); Side). apply HNCol2; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2