proposition: Lemma concyclic_gen_perm_2 : forall A B C D, Concyclic_gen A B C D -> Concyclic_gen B A C D.
proof: Proof. intros A B C D [H|]. left; apply concyclic_perm_2, H. right; spliter; repeat split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel