proposition: Lemma l6_4_2 : forall A B P, Col A P B /\ ~ Bet A P B -> Out P A B.
proof: Proof. unfold Col. intros. spliter. unfold Out. induction H. contradiction. induction (eq_dec_points A P). subst P; intuition. induction (eq_dec_points B P). subst P; intuition. induction H; repeat split; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le