proposition: Lemma col_proj_proj : forall A B A' P Q, A <> A' -> Col A B A' -> proj A P Q A' -> proj B P Q A'.
proof: Proof. intros. unfold proj in *. spliter. induction H2; spliter; split;auto. induction(col_dec P Q B). right. split. assumption. induction(eq_dec_points A' P). subst P. assert(Perp_at A' A' Q A A'). eapply perp_perp_in. assumption. eapply l8_14_2_1b. apply H6. Col. Col. assert(Perp P A' A A'). eapply perp_col. auto. apply H3. assumption. assert(Perp_at A' A' P A A'). eapply perp_perp_in. Perp. induction(eq_dec_points B P). subst P. assert(Perp B Q A B). apply perp_sym. eapply perp_col. intro. subst B. apply H2. Col. apply perp_sym. apply H3. Col. eapply l8_14_2_1b. apply H8. Col. Col. assert(Perp P B A B). eapply perp_col. auto. apply perp_sym. eapply perp_col. intro. subst B. contradiction. apply perp_sym. apply H3. Col. Col. eapply l8_14_2_1b. apply H8. ColR. Col. left. repeat split; auto. apply perp_sym. apply perp_left_comm. eapply perp_col. intro. subst A'. contradiction. apply perp_sym. apply perp_right_comm. apply H3. Col. subst A'. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec