proposition: Lemma proj3_col : forall A B C A' B' C' P Q , proj A P Q A' -> proj B P Q B' -> proj C P Q C' -> Col A' B' C'.
proof: Proof. intros. unfold proj in *. spliter. induction H4; induction H3; induction H2; spliter. eapply (col3 P Q); Col. subst C'. eapply (col3 P Q); Col. subst B'. eapply (col3 P Q); Col. subst C'. subst B'. eapply (col3 P Q); Col. subst A'. eapply (col3 P Q); Col. subst C'. subst A'. eapply (col3 P Q); Col. subst A'. subst B'. eapply (col3 P Q); Col. subst A'. subst B'. subst C'. eapply (col3 P Q); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec