proposition: Lemma proj_par_strict : forall A B A' B' P Q, A <> A' -> B <> B' -> A' <> B' -> proj A P Q A' -> proj B P Q B' -> Par_strict A A' B B'.
proof: Proof. intros. assert(Par A A' B B'). eapply (proj_par A B A' B' P Q); auto. induction H4. assumption. spliter. unfold Par_strict. repeat split; auto; try apply all_coplanar. intro. ex_and H8 X. assert(~Col P Q A). eapply proj_not_col. apply H. assumption. assert(~Col P Q B). eapply proj_not_col. apply H0. assumption. assert(A <> B). eapply proj_not_eq. apply H1. apply H2. assumption. assert(Col A' P Q). eapply proj_col. apply H2. assert(Col B' P Q). eapply proj_col. apply H3. apply H1. eapply (l6_21 P Q). apply H11. apply H0. Col. Col. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec