proposition: Lemma cop_par_perp__perp : forall A B C D P Q, Par A B C D -> Perp A B P Q -> Coplanar C D P Q -> Perp C D P Q.
proof: Proof. apply universal_posidonius_postulate__perpendicular_transversal_postulate. apply playfair__universal_posidonius_postulate. unfold playfair_s_postulate; apply parallel_uniqueness. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID