proposition: Lemma acute_bet__obtuse : forall A B C A', Bet A B A' -> A' <> B -> Acute A B C -> Obtuse A' B C.
proof: Proof. intros A B C A' HBet HA'B Hacute. assert(Hd := acute_distincts A B C Hacute). destruct Hd. elim(col_dec A B C). { intro. elim(bet_dec A B C). - intro. exfalso. apply (nlta A B C). apply acute_obtuse__lta; auto. apply bet__obtuse; auto. - intro. apply bet__obtuse; auto. apply between_symmetry. apply (l6_2 A); auto. 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 acute_per__lta; auto. apply (per_col _ _ D); Perp; Col. } assert(OS B A' C D) by (apply (col_one_side _ A); Side; Col). exists A, B, D. split; Perp. split. - exists D. split; [|apply conga_comm, l11_18_1; Perp]. apply os2__inangle; auto. exists A. split. { repeat split; Col. intro; apply HNCol1; ColR. 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); Side. apply lta__lea. apply acute_per__lta; Perp. - intro. apply HNCol2. assert (Out B D C). apply (conga_os__out A'); Side. apply (conga_trans _ _ _ A B D); auto. apply l11_16; auto; apply (l8_3 A); Perp; Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2