proposition: Lemma third_point : forall A B P, Col A B P -> Bet P A B \/ Bet A P B \/ Bet A B P.
proof: Proof. intros. induction H. right; right. auto. induction H. right; left. Between. left. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col