proposition: Lemma cop_tsp__ex_cop2 : forall A B C D E P, Coplanar A B C P -> TSP A B C D E -> exists Q, Coplanar A B C Q /\ Coplanar D E P Q /\ P <> Q.
proof: Proof. intros A B C D E P HCop HTSP. destruct (col_dec D E P) as [|HNCol]. { apply tsp_distincts in HTSP; spliter. destruct (eq_dec_points P A). subst; exists B; repeat split; Cop. exists A; repeat split; Cop. } destruct HTSP as [_ [_ [Q []]]]. exists Q; repeat split; Cop. intro; subst; apply HNCol; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar