proposition: Lemma project_pj : forall P P' A B X Y, Proj P P' A B X Y -> Pj X Y P P'.
proof: Proof. intros. unfold Proj in H. spliter. unfold Pj. induction H3. left. apply par_symmetry. auto. right. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum