proposition: Lemma col_obtuse__bet : forall A B C, Col A B C -> Obtuse A B C -> Bet A B C.
proof: Proof. intros. destruct H0 as [X [Y [Z []]]]. apply (col_lta__bet X Y Z); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2