proposition: Lemma par_col_project : forall P P' A B X Y , A <> B -> ~ Par A B X Y -> Par P P' X Y -> Col A B P' -> Proj P P' A B X Y.
proof: Proof. intros. apply par_distincts in H1. spliter. unfold Proj. repeat split;auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors