proposition: Lemma proj_perp_id : forall A B C A' B' P Q, A <> C -> Col A B C -> proj A P Q A' -> proj B P Q B' -> proj C P Q A' -> A' = B'.
proof: Proof. intros. induction(eq_dec_points A A'). subst A'. apply proj_id with C B P Q; Col. assert(Col A C A'). eapply proj_eq_col. apply H1. assumption. assert(Col A B A'). ColR. eapply proj_id. apply H4. apply H6. apply H1. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec