proposition: Lemma per_proj : forall A B T P, A <> B -> Per T P A -> Per T P B -> Col A B P -> proj T A B P.
proof: Proof. intros. unfold proj. split; auto. induction (col_dec A B T). right. split; auto. assert(Col T P A). ColR. assert(Col T P B). ColR. induction(eq_dec_points A P). subst P. assert(T=A \/ B=A). apply l8_9; auto. induction H6. auto. subst B. tauto. assert(T=P \/ A=P). apply l8_9; auto. induction H7. auto. subst P. tauto. left. induction (eq_dec_points A P). subst P. repeat split; auto. apply per_perp_in in H1. apply perp_in_comm in H1. apply perp_in_perp_bis in H1. induction H1. Perp. apply perp_not_eq_1 in H1. tauto. intro. subst T. contradiction. assumption. repeat split; auto. apply per_perp_in in H0. apply perp_in_comm in H0. apply perp_in_perp_bis in H0. induction H0. eapply perp_col. assumption. eauto with perp. Col. apply perp_not_eq_1 in H0. tauto. intro. subst T. contradiction. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec