proposition: Lemma concours_non_paralleles : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> ~ alignes A B D -> concours (droite C D) (droite A B) -> ~ paralleles (droite C D) (droite A B).
proof: Proof. intros A B C D H10 H20 H H0; try assumption. cut (~ ~ concours (droite C D) (droite A B)); intros. unfold not in |- *; intros. apply H1. apply paralleles_non_concours; auto. intuition. Qed.