proposition: Lemma concyclic_trans_1 : forall P Q R A B, ~ Col P Q R -> Concyclic P Q R A -> Concyclic P Q R B -> Concyclic Q R A B.
proof: Proof. intros P Q R A B HNC H1 H2. split. unfold Concyclic in *; spliter; apply coplanar_trans_1 with P; assumption. destruct (concyclic_aux P Q R A H1) as [O [M]]. destruct (concyclic_aux P Q R B H2) as [O' [M']]. spliter. exists O, M; repeat split; trivial. assert_diffs. apply (cop2_onc6__eqc P Q R O' M'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel