proposition: Lemma cop3_tsp__tsp : forall A B C D E F P Q, ~ Col D E F -> Coplanar A B C D -> Coplanar A B C E -> Coplanar A B C F -> TSP A B C P Q -> TSP D E F P Q.
proof: Proof. intros A B C D E F P Q HNCol HD HE HF [HP [HQ [T [HT HBet]]]]. assert (~ Col A B C) by (apply ncop__ncol with P, HP). assert (Coplanar D E F A /\ Coplanar D E F B /\ Coplanar D E F C /\ Coplanar D E F T). repeat split; apply coplanar_pseudo_trans with A B C; Cop. spliter. repeat split. intro; apply HP; apply coplanar_pseudo_trans with D E F; Cop. intro; apply HQ; apply coplanar_pseudo_trans with D E F; Cop. exists T; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar