proposition: Lemma par_col_par_2 : forall A B C D P, A <> P -> Col A B P -> Par A B C D -> Par A P C D.
proof: Proof. intros. apply par_symmetry. apply par_symmetry in H1. apply par_col_par with B; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles