proposition: Lemma project_col_project : forall A B C P P' X Y, A <> C -> Col A B C -> Proj P P' A B X Y -> Proj P P' A C X Y.
proof: Proof. intros. unfold Proj in *. spliter. repeat split; auto. intro. apply H3. eapply (par_col_par_2 _ C); Col; Par. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg