proposition: Lemma proj_per : forall A B T P, A <> B -> proj T A B P -> Per T P A /\ Per T P B /\ Col A B P.
proof: Proof. intros. unfold proj in H0. spliter. induction H1. spliter. repeat split. induction (eq_dec_points A P). treat_equalities. apply l8_5. apply perp_in_per. eauto with perp. induction (eq_dec_points B P). treat_equalities. apply l8_5. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. eapply perp_col. assumption. eauto with perp. Col. assumption. spliter. subst T. repeat split. Perp. Perp. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec