proposition: Lemma col_par_par_col : forall A B C A' B' C', Col A B C -> Par A B A' B' -> Par B C B' C' -> Col A' B' C'.
proof: Proof. intros. apply par_distincts in H0. apply par_distincts in H1. spliter. assert(Par A B B C). right. repeat split; Col. assert(Par A' B' B' C'). apply (par_trans _ _ A' B'). Par. apply (par_trans _ _ B C). apply (par_trans _ _ A B); Par. Par. induction H7. apply False_ind. apply H7. exists B'. split; Col. spliter. Col. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID