proposition: Lemma project_project_par : forall P P' A B X Y X' Y', P <> P' -> Proj P P' A B X Y -> Proj P P' A B X' Y' -> Par X Y X' Y'.
proof: Proof. intros. unfold Proj in *. spliter. induction H9; induction H5; try contradiction. eapply par_trans. apply par_symmetry. apply H9. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors