proposition: Lemma tsp_exists : forall A B C P, ~ Coplanar A B C P -> exists Q, TSP A B C P Q.
proof: Proof. intros A B C P HP. destruct (segment_construction P A A P) as [Q []]. assert (HA : Coplanar A B C A) by Cop. exists Q; repeat split. - assumption. - assert (A <> P) by (intro; subst; apply HP, HA); assert_diffs. intro; apply HP, col_cop2__cop with A Q; Col. - exists A; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar