proposition: Lemma proj3_id : forall A B C C' P Q, A <> B -> Col A B C -> proj A P Q A -> proj B P Q B -> proj C P Q C' -> C = C'.
proof: Proof. intros. assert(Col A B C'). eapply (proj3_col A B C A B C' P Q); auto. assert(HH1:= H1). assert(HH2:=H2). assert(HH3:=H3). unfold proj in HH1. unfold proj in HH2. unfold proj in HH3. spliter. induction H10; induction H8; induction H6; spliter. apply perp_not_eq_2 in H15. tauto. apply perp_not_eq_2 in H14. tauto. apply perp_not_eq_2 in H14. tauto. apply perp_not_eq_2 in H13. tauto. apply perp_not_eq_2 in H13. tauto. apply perp_not_eq_2 in H12. tauto. assert(Col P A B). ColR. assert(Col Q A B). ColR. assert(Col P Q C). eapply (col3 A B); Col; eapply (l8_14_2_1b_bis _ _ _ _ C') in H7. contradiction. subst C. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec