proposition: Lemma col_lta__out : forall A B C X Y Z, Col A B C -> LtA A B C X Y Z -> Out B A C.
proof: Proof. intros. apply not_bet_out. assumption. intro. destruct H0. apply H2. apply lea_asym. assumption. apply lea_distincts in H0. spliter. apply l11_31_2; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2