proposition: Lemma bet__obtuse : forall A B C, Bet A B C -> A <> B -> B <> C -> Obtuse A B C.
proof: Proof. intros A B C HBet HAB HBC. assert(HD := perp_exists B A B). destruct HD as [D]; auto. assert_diffs. exists A. exists B. exists D. split; Perp. split. apply l11_31_2; auto. intro. assert(HNCol : ~ Col A B D) by (apply per_not_col; Perp). apply HNCol. apply bet_col. apply (bet_conga__bet A B C); try (apply conga_sym); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2