proposition: Lemma project_par_project : forall P P' A B X Y X' Y', Proj P P' A B X Y -> Par X Y X' Y' -> Proj P P' A B X' Y'.
proof: Proof. intros. unfold Proj in *. spliter. apply par_distincts in H0. spliter. repeat split; Col. intro. apply H2. eapply par_trans. apply H7. Par. induction H4. left. eapply par_trans. apply H4. assumption. right. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors