proposition: Lemma coplanar_perm_3 : forall A B C D, Coplanar A B C D -> Coplanar A C D B.
proof: Proof. intros A B C D HCop. destruct HCop as [X H]; exists X. induction H; try (induction H); spliter; Col5. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality