proposition: Lemma coplanar_pseudo_trans : forall A B C D P Q R, ~ Col P Q R -> Coplanar P Q R A -> Coplanar P Q R B -> Coplanar P Q R C -> Coplanar P Q R D -> Coplanar A B C D.
proof: Proof. assert (Haux : forall P Q R A B C, ~ Col P Q R -> Coplanar P Q R A -> Coplanar P Q R B -> Coplanar P Q R C -> Coplanar A B C R). { intros P Q R A B C HNC HCop1 HCop2 HCop3. assert_diffs. elim (col_dec R Q A); intro HQRA. apply coplanar_perm_18, col_cop__cop with Q; auto. apply coplanar_perm_17, (coplanar_trans_1 P); assumption. apply coplanar_perm_9, (coplanar_trans_1 Q); [Col|apply (coplanar_trans_1 P); assumption..]. } intros A B C D P Q R HNC HCop1 HCop2 HCop3 HCop4. elim (col_dec P Q D); intro HPQD. apply col_cop2__cop with P Q; [assert_diffs|apply (Haux Q R)|apply (Haux P R)|]; Col; Cop. apply (Haux P Q); [assumption|apply (coplanar_trans_1 R); Col; Cop..]. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar