proposition: Lemma l9_39 : forall A B C D P Q R, TSP A B C P R -> Coplanar A B C D -> Out D P Q -> TSP A B C Q R.
proof: Proof. intros A B C D P Q R [HP [HR [T [HT HBet]]]] HCop HOut. assert (HNCol : ~ Col A B C) by (apply ncop__ncol with P, HP). split. intro; assert_diffs; apply HP, col_cop2__cop with D Q; Col. split; [assumption|]. destruct (eq_dec_points D T). subst T; exists D; split; [|apply (bet_out__bet P)]; assumption. assert (HTS : TS D T Q R). { assert (~ Col P D T) by (intro; apply HP, col_cop2__cop with D T; Col). apply l9_8_2 with P. - repeat split; auto. intro; apply HR, col_cop2__cop with D T; Col. exists T; split; Col. - apply out_one_side; Col. } destruct HTS as [HNCol1 [HNCol2 [T' []]]]. exists T'; split; [|assumption]. apply col_cop2__cop with D T; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar