proposition: Lemma col_in_angle_out : forall A B C P, Col B A P -> ~ Bet A B C -> InAngle P A B C -> Out B A P.
proof: Proof. intros. unfold InAngle in H1. spliter. ex_and H4 X. induction H5. subst X. contradiction. induction (eq_dec_points A X). subst X. assumption. apply not_bet_out in H0. assert(Out B A P /\ Out B C P). eapply out2_bet_out. assumption. apply H5. assumption. spliter. assumption. assert (Col B A X). apply col_transitivity_1 with P; Col. apply col_transitivity_2 with X; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2