proposition: Lemma Cop_3142 : forall A B C D, Cop A B C D -> Cop C A D B.
proof: Proof. intros A B C D [E [F [G]]]; spliter; exists E, F, G; repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.coplanar GeoCoq.Tarski_dev.Ch09_plane