proposition: Lemma Copl_1342 : forall A B C D, Copl A B C D -> Copl A C 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