proposition: Lemma pj_col_project : forall P P' A B X Y, A <> B -> X <> Y -> Col P' A B -> ~ Par A B X Y -> Pj X Y P P' -> Proj P P' A B X Y.
proof: Proof. intros. unfold Pj in H3. induction H3. unfold Proj. repeat split; Col. left. apply par_symmetry. assumption. subst P'. apply project_trivial; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg