proposition: Lemma cop2_ts__tsp : forall A B C D E X Y, ~ Coplanar A B C X -> Coplanar A B C D -> Coplanar A B C E -> TS D E X Y -> TSP A B C X Y.
proof: Proof. intros A B C D E X Y HX HD HE [HNCol [HNCol' [T []]]]. assert (Coplanar A B C T) by (assert_diffs; apply col_cop2__cop with D E; Col). repeat split. assumption. intro; apply HX, col_cop2__cop with T Y; Col; intro; subst; apply HNCol'; Col. exists T; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar