proposition: Lemma concyclic_perm_2 : forall A B C D, Concyclic A B C D -> Concyclic B A C D.
proof: Proof. unfold Concyclic. intros A B C D [HCop [O [P]]]. split. Cop. exists O, P. spliter; repeat split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel