[STATEMENT]
lemma cop_not_par_other_side:
  assumes "C \<noteq> D" and
    "Col A B I" and
    "Col C D I" and
    "\<not> Col A B C" and
    "\<not> Col A B P" and
    "Coplanar A B C P"
  shows "\<exists> Q. Col C D Q \<and> A B TS P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
obtain X Y where P1:"Col C D X \<and> Col C D Y \<and> A B TS X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X Y. Col C D X \<and> Col C D Y \<and> A B TS X Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) assms(2) assms(3) assms(4) not_par_two_sides
[PROOF STATE]
proof (prove)
using this:
C \<noteq> D
Col A B I
Col C D I
\<not> Col A B C
\<lbrakk>?C \<noteq> ?D; Col ?A ?B ?I; Col ?C ?D ?I; \<not> Col ?A ?B ?C\<rbrakk> \<Longrightarrow> \<exists>X Y. Col ?C ?D X \<and> Col ?C ?D Y \<and> ?A ?B TS X Y

goal (1 subgoal):
 1. (\<And>X Y. Col C D X \<and> Col C D Y \<and> A B TS X Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col C D X \<and> Col C D Y \<and> A B TS X Y

goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col C D X \<and> Col C D Y \<and> A B TS X Y
[PROOF STEP]
have "Coplanar C A B X"
[PROOF STATE]
proof (prove)
using this:
Col C D X \<and> Col C D Y \<and> A B TS X Y

goal (1 subgoal):
 1. Coplanar C A B X
[PROOF STEP]
using Coplanar_def assms(1) assms(2) assms(3) col_transitivity_1
[PROOF STATE]
proof (prove)
using this:
Col C D X \<and> Col C D Y \<and> A B TS X Y
Coplanar ?A ?B ?C ?D \<equiv> \<exists>X. Col ?A ?B X \<and> Col ?C ?D X \<or> Col ?A ?C X \<and> Col ?B ?D X \<or> Col ?A ?D X \<and> Col ?B ?C X
C \<noteq> D
Col A B I
Col C D I
\<lbrakk>?P \<noteq> ?Q; Col ?P ?Q ?A; Col ?P ?Q ?B\<rbrakk> \<Longrightarrow> Col ?P ?A ?B

goal (1 subgoal):
 1. Coplanar C A B X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Coplanar C A B X

goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Coplanar C A B X
[PROOF STEP]
have "Coplanar A B P X"
[PROOF STATE]
proof (prove)
using this:
Coplanar C A B X

goal (1 subgoal):
 1. Coplanar A B P X
[PROOF STEP]
using assms(4) assms(6) col_permutation_3 coplanar_trans_1 ncoplanar_perm_2 ncoplanar_perm_6
[PROOF STATE]
proof (prove)
using this:
Coplanar C A B X
\<not> Col A B C
Coplanar A B C P
Col ?A ?B ?C \<Longrightarrow> Col ?C ?B ?A
\<lbrakk>\<not> Col ?P ?Q ?R; Coplanar ?P ?Q ?R ?A; Coplanar ?P ?Q ?R ?B\<rbrakk> \<Longrightarrow> Coplanar ?Q ?R ?A ?B
\<not> Coplanar ?A ?B ?C ?D \<Longrightarrow> \<not> Coplanar ?A ?C ?B ?D
\<not> Coplanar ?A ?B ?C ?D \<Longrightarrow> \<not> Coplanar ?B ?A ?C ?D

goal (1 subgoal):
 1. Coplanar A B P X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Coplanar A B P X

goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Coplanar A B P X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Coplanar A B P X

goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
by (meson P1 l9_8_2 TS_def assms(5) cop_nts__os not_col_permutation_2 one_side_symmetry)
[PROOF STATE]
proof (state)
this:
\<exists>Q. Col C D Q \<and> A B TS P Q

goal:
No subgoals!
[PROOF STEP]
qed