proposition: Lemma concyclic_gen_pseudo_trans : forall A B C D P Q R, ~ Col P Q R -> Concyclic_gen P Q R A -> Concyclic_gen P Q R B -> Concyclic_gen P Q R C -> Concyclic_gen P Q R D -> Concyclic_gen A B C D.
proof: Proof. intros A B C D P Q R HNC [|] [|] [|] [|]; [|spliter; exfalso; apply HNC; Col..]. left. apply concyclic_pseudo_trans with P Q R; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel