proposition: Lemma project_col_eq : forall P Q P' Q' A B X Y, P <> P' -> Col P Q P' -> Proj P P' A B X Y -> Proj Q Q' A B X Y -> P' = Q'.
proof: Proof. intros. induction(eq_dec_points P Q). subst Q. eapply project_uniqueness. apply H1. apply H2. eapply project_par. apply H1. apply H2. unfold Proj in *. spliter. induction H11; induction H7. eapply (par_col_par_2 _ P'); Col. subst Q'. eapply (par_col_par_2 _ P'); Col. contradiction. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors