proposition: Lemma cop_par__perp2 : forall A B C D P, Coplanar A B C P -> Par A B C D -> Perp2 A B C D P.
proof: Proof. intros. apply par_distincts in H0. spliter. unfold Perp2. assert(HH:= ex_perp_cop A B P C H1). ex_and HH Q. exists P. exists Q. repeat split. Col. Perp. apply perp_sym. apply (cop_par_perp__perp A B); Perp. apply par_symmetry in H0. induction H0. apply coplanar_pseudo_trans with A B C; Cop. apply par_strict_not_col_3 with D. assumption. spliter. apply coplanar_perm_16, col2_cop__cop with A B; Col; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project