proposition: Lemma cop3_tsp__ts : forall A B C D E X Y, D <> E -> Coplanar A B C D -> Coplanar A B C E -> Coplanar D E X Y -> TSP A B C X Y -> TS D E X Y.
proof: Proof. intros A B C D E X Y HDE HD HE HCop HTSP. assert (HX : ~ Coplanar A B C X) by (apply tsp__ncop1 with Y, HTSP). assert (HY : ~ Coplanar A B C Y) by (apply tsp__ncop2 with X, HTSP). apply cop_nos__ts. assumption. intro; apply HX, col_cop2__cop with D E; Col. intro; apply HY, col_cop2__cop with D E; Col. intro. apply tsp__nosp in HTSP. apply HTSP, cop2_os__osp with D E; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar