proposition: Lemma paralleles_non_concours : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> ~ alignes A B D -> paralleles (droite C D) (droite A B) -> ~ concours (droite C D) (droite A B).
proof: Proof. intros A B C D H10 H11 H H0. elim def_paralleles2 with (3 := H0); intros; auto. unfold not in |- *; intros. elim def_concours2 with (3 := H2); intros; auto. elim H3; [ intros H4 H5; try clear H3; try exact H5 ]. elim H4; clear H4; (unfold alignes1 in |- *; intros); [ tauto | idtac ]. elim H3; [ intros k H4; try clear H3; try exact H4 ]. elim H5; clear H5; (unfold alignes1 in |- *; intros); [ tauto | idtac ]. elim H3; [ intros k0 H5; try clear H3; try exact H5 ]. apply H. cut (add_PP (cons k0 A) (cons (1 + - k0) B) = add_PP (cons k C) (cons (1 + - k) D)); intros. unfold alignes, alignes1 in |- *. right; try assumption. exists (k0 + - (x * k)). pattern 1 at 1 in |- *. replace 1 with (k + (1 + - k)); try ring. replace (cons (k + (1 + - k)) D) with (add_PP (cons k D) (cons (1 + - k) D)). replace (cons k D) with (mult_PP k (cons 1 D)). RingPP1 H1. replace (cons (k0 + - (x * k)) A) with (add_PP (cons k0 A) (cons (- (x * k)) A)). replace (1 + - (k0 + - (x * k))) with (1 + - k0 + x * k); try ring. RingPP1 H3. RingPP. RingPP. RingPP. RingPP. rewrite <- H4; auto. Qed.