proposition: Lemma perp2_trans : forall A B C D E F P, Perp2 A B C D P -> Perp2 C D E F P -> Perp2 A B E F P.
proof: Proof. intros. unfold Perp2 in *. ex_and H X. ex_and H1 Y. ex_and H0 X'. ex_and H3 Y'. assert(Par X Y X' Y'). apply (l12_9_2D _ _ _ _ C D); Perp. exists X. exists Y. assert(Col X X' Y'). induction H5. unfold Par_strict in H5. spliter. apply False_ind. apply H6. exists P. split; Col. spliter. auto. assert(Col Y X' Y'). induction H5. unfold Par_strict in H5. spliter. apply False_ind. apply H7. exists P. split; Col. spliter. auto. repeat split; auto. assert(X <> Y). apply perp_not_eq_1 in H1. assert(X' <> Y'). apply perp_not_eq_1 in H3. auto. 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 H5. induction H5. unfold Par_strict in H5. spliter. apply False_ind. apply H10. exists P. split; Col. spliter. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel