proposition: Lemma par__coplanar : forall A B C D, Par A B C D -> Coplanar A B C D.
proof: Proof. intros A B C D H. destruct H. apply pars__coplanar; assumption. spliter; exists A; left; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality