proposition: Lemma acute_col__out : forall A B C, Col A B C -> Acute A B C -> Out B A C.
proof: Proof. intros. destruct H0 as [X [Y [Z []]]]. apply col_lta__out with X Y Z; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2