proposition: Lemma col_not_col_not_par : forall A B C D, (exists P, Col A B P /\ Col C D P) -> (exists Q, Col C D Q /\ ~Col A B Q) -> ~Par A B C D.
proof: Proof. intros. ex_and H P. ex_and H0 Q. intro. unfold Par in H3. induction H3. unfold Par_strict in H3. spliter. apply H4. exists P. Col5. spliter. apply H2. eapply col3. apply H4. Col. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles