proposition: Lemma concyclic_pseudo_trans : forall A B C D P Q R, ~ Col P Q R -> Concyclic P Q R A -> Concyclic P Q R B -> Concyclic P Q R C -> Concyclic P Q R D -> Concyclic A B C D.
proof: Proof. intros A B C D P Q R HNCol HA HB HC HD. spliter. split. unfold Concyclic in *; spliter; apply coplanar_pseudo_trans with P Q R; assumption. destruct (concyclic_aux P Q R A HA) as [OA [MA]]. destruct (concyclic_aux P Q R B HB) as [OB [MB]]. destruct (concyclic_aux P Q R C HC) as [OC [MC]]. destruct (concyclic_aux P Q R D HD) as [OD [MD]]. spliter. assert_diffs. exists OA, MA; repeat split; [|apply (cop2_onc6__eqc P Q R OB MB)| apply (cop2_onc6__eqc P Q R OC MC)|apply (cop2_onc6__eqc P Q R OD MD)]; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel