proposition: Lemma droites_non_paralleles : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> ~ paralleles (droite C D) (droite A B) -> concours (droite C D) (droite A B) \/ ~ coplanaires A B C D.
proof: Proof. intros A B C D H20 H21 H; try assumption. elim (classic (coplanaires A B C D)); intros. left; try assumption. hPPcoplanaires H0 a b. apply def_concours with C; auto with geo. cut (a + b <> 0); intros. apply def_concours with (barycentre (cons a A) (cons b B)); auto. replace (barycentre (cons a A) (cons b B)) with (barycentre (cons (- (1 + - (a + b))) C) (cons 1 D)). apply barycentre_alignes. replace (- (1 + - (a + b)) + 1) with (a + b); auto. ring. apply conversion_PP with (a := - (1 + - (a + b)) + 1) (b := a + b). rewrite <- add_PP_barycentre; auto. rewrite <- add_PP_barycentre; auto. rewrite H0. RingPP. replace (- (1 + - (a + b)) + 1) with (a + b); auto. ring. replace (- (1 + - (a + b)) + 1) with (a + b); auto. ring. ring. apply barycentre_alignes; auto. unfold not in |- *; intros; apply H. apply def_paralleles with (- a); auto. rewrite H0. rewrite H1. replace b with (- a + (a + b)); auto. rewrite H1. RingPP. ring. right; try assumption. Qed.