proposition: Lemma project_id : forall A B X Y P P', Proj P P' A B X Y -> Col A B P -> P = P'.
proof: Proof. intros. unfold Proj in H. spliter. induction H4. apply False_ind. apply H2. induction(eq_dec_points P' A). subst P'. eapply (par_col_par_2 _ P); Col. Par. eapply (par_col_par_2 _ P'); Col. apply par_left_comm. eapply (par_col_par_2 _ P); Col. ColR. Par. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors