proposition: Lemma par_col_par : forall A B C D D', C <> D' -> Par A B C D -> Col C D D' -> Par A B C D'.
proof: Proof. intros. unfold Par in *. induction H0. left. assert_diffs. unfold Par_strict in *. spliter. split. apply col_cop__cop with D; auto. intro. apply H2. ex_and H8 P. exists P. split. assumption. apply col_permutation_2. eapply col_transitivity_1. apply H. Col. Col. right. spliter. repeat split. assumption. assumption. apply col_permutation_2. eapply col_transitivity_1. apply H2. assumption. Col. apply col_permutation_2. eapply col_transitivity_1. apply H2. assumption. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles