proposition: Lemma perp2_pseudo_trans : forall A B C D E F P, Perp2 A B C D P -> Perp2 C D E F P -> ~ Col C D P -> Perp2 A B E F P.
proof: Proof. intros. unfold Perp2 in *. ex_and H X. ex_and H2 Y. ex_and H0 X'. ex_and H4 Y'. assert(Par X Y X' Y'). assert(Coplanar P C D X). induction(eq_dec_points X P). subst. exists P. left. split; Col. apply coplanar_perm_9. apply perp__coplanar. apply perp_col with Y; Col. assert(Coplanar P C D Y). induction(eq_dec_points Y P). subst. exists P. left. split; Col. apply coplanar_perm_9. apply perp__coplanar. apply perp_col with X; Perp; Col. assert(Coplanar P C D X'). induction(eq_dec_points X' P). subst. exists P. left. split; Col. apply coplanar_perm_9. apply perp__coplanar. apply perp_col with Y'; Col. assert(Coplanar P C D Y'). induction(eq_dec_points Y' P). subst. exists P. left. split; Col. apply coplanar_perm_9. apply perp__coplanar. apply perp_col with X'; Perp; Col. apply (l12_9 _ _ _ _ C D); Perp; apply coplanar_trans_1 with P; Col. exists X. exists Y. assert(Col X X' Y'). induction H6. unfold Par_strict in H6. spliter. apply False_ind. apply H7. exists P. split; Col. spliter. auto. assert(Col Y X' Y'). induction H6. unfold Par_strict in H6. spliter. apply False_ind. apply H8. exists P. split; Col. spliter. auto. repeat split; auto. assert(X <> Y). apply perp_not_eq_1 in H2. auto. induction(eq_dec_points X Y'). subst Y'. apply (perp_col _ X'). auto. Perp. ColR. apply (perp_col _ Y'). auto. apply perp_left_comm. apply(perp_col _ X'). auto. Perp. ColR. apply par_symmetry in H6. induction H6. unfold Par_strict in H6. spliter. apply False_ind. apply H11. exists P. split; Col. spliter. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel