proposition: Lemma col_cop_perp2__pars_bis : forall P A B C D, ~ Col A B P -> Col C D P -> Coplanar A B C D -> Perp2 A B C D P -> Par_strict A B C D.
proof: Proof. unfold Perp2. intros. ex_and H2 X. ex_and H3 Y. assert (Col X Y P) by Col. assert (HQ := diff_col_ex3 X Y P H5). ex_and HQ Q. apply (col_cop_perp2__pars P Q); trivial; apply perp_col0 with X Y; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel