proposition: Lemma proj_col_proj : forall A B C T P, proj T A B P -> A <> C -> Col A B C -> proj T A C P.
proof: Proof. intros. unfold proj in *. spliter. induction H2; repeat split; auto; spliter. left. repeat split. intro. apply H2. ColR. eapply (perp_col _ B); auto. ColR. subst T. right. split; auto. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec