proposition: Lemma bet_cop__tsp : forall A B C X Y P, ~ Coplanar A B C X -> P <> Y -> Coplanar A B C P -> Bet X P Y -> TSP A B C X Y.
proof: Proof. intros A B C X Y P HX HPY HP HBet. apply (l9_18_3 A B C X Y P); Col. repeat split; [assumption..|]. intro; apply HX, col_cop2__cop with P Y; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar