[STATEMENT]
lemma coplanar_perm_18:
  assumes "Coplanar A B C D"
  shows "Coplanar D A B C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
obtain X where P1: "(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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>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 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Coplanar_def assms
[PROOF STATE]
proof (prove)
using this:
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
Coplanar A B C D

goal (1 subgoal):
 1. (\<And>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 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
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

goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
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
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
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

goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
using Coplanar_def col_permutation_4
[PROOF STATE]
proof (prove)
using this:
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
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
Col ?A ?B ?C \<Longrightarrow> Col ?B ?A ?C

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

goal:
No subgoals!
[PROOF STEP]
qed