proposition: Lemma col_cop_perp2__pars : forall P Q A B C D, ~ Col A B P -> Col C D P -> Coplanar A B C D -> Perp A B P Q -> Perp C D P Q -> Par_strict A B C D.
proof: Proof. intros. apply par_not_col_strict with P; trivial. assert_diffs. assert (Coplanar A B C P) by (apply col_cop__cop with D; Col). assert (Coplanar A B D P) by (apply col_cop__cop with C; Col; Cop). apply l12_9 with P Q; trivial; apply coplanar_perm_2. apply coplanar_trans_1 with B; Col; Cop. apply coplanar_trans_1 with B; Col; Cop. apply coplanar_trans_1 with A; Col; Cop. apply coplanar_trans_1 with A; Col; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles