proposition: Lemma perp2_perp_in : forall A B C D O, Perp2 A B C D O -> ~Col O A B /\ ~Col O C D -> exists P, exists Q, Col A B P /\ Col C D Q /\ Col O P Q /\ Perp_at P O P A B /\ Perp_at Q O Q C D.
proof: Proof. intros. unfold Perp2 in H. ex_and H X. ex_and H1 Y. assert(X <> Y). apply perp_not_eq_1 in H2. auto. assert(HH:= perp_inter_perp_in_n X Y A B H2). ex_and HH P. assert(HH:= perp_inter_perp_in_n X Y C D H3). ex_and HH Q. exists P. exists Q. split; auto. split; auto. split. apply (col3 X Y); Col. split. induction(eq_dec_points X O). subst X. apply perp_in_sym. apply(perp_in_col_perp_in A B O Y P P). intro. subst P. apply H. Col. Col. apply perp_in_sym. auto. assert(Perp_at P A B X O). apply(perp_in_col_perp_in A B X Y O P H11). Col. apply perp_in_sym. auto. apply perp_in_right_comm in H12. eapply (perp_in_col_perp_in _ _ _ _ P) in H12 . apply perp_in_sym. auto. intro. subst P. apply H. Col. ColR. induction(eq_dec_points X O). subst X. apply perp_in_sym. apply(perp_in_col_perp_in C D O Y Q Q). intro. subst Q. apply H0. Col. Col. apply perp_in_sym. auto. assert(Perp_at Q C D X O). apply(perp_in_col_perp_in C D X Y O Q H11). Col. apply perp_in_sym. auto. apply perp_in_right_comm in H12. eapply (perp_in_col_perp_in _ _ _ _ Q) in H12 . apply perp_in_sym. auto. intro. subst Q. apply H0. Col. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel