proposition: Lemma proj_par : forall A B A' B' P Q, A <> A' -> B <> B' -> proj A P Q A' -> proj B P Q B' -> Par A A' B B'.
proof: Proof. intros. eapply l12_9_2D. unfold proj in *. spliter. induction H4; induction H3; spliter. apply perp_sym. apply H7. Perp. subst A'. tauto. subst B'. tauto. unfold proj in *. spliter. induction H4; induction H3; spliter. apply perp_sym. apply H5. subst B'. tauto. subst A'. tauto. subst A'. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec