proposition: Lemma par_col2_par : forall A B C D E F, E <> F -> Par A B C D -> Col C D E -> Col C D F -> Par A B E F.
proof: Proof. intros. induction (eq_dec_points C E). subst E. eapply par_col_par. assumption. apply H0. assumption. eapply par_col_par. assumption. apply par_right_comm. eapply par_col_par. apply H3. apply H0. assumption. apply col_permutation_2. eapply col_transitivity_1. apply par_distincts in H0. spliter. apply H5. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles