proposition: Lemma concours_coplanaires : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> concours (droite A B) (droite C D) -> coplanaires A B D C.
proof: Proof. unfold coplanaires in |- *; intros A B C D H20 H21 H11. elim def_concours2 with (A := A) (B := B) (C := C) (D := D); [ intros I H0; elim H0; intros H1 H2; try clear H0; try exact H2 | auto | auto | auto ]. hPPalignes H2 k. hPPalignes H1 k0. cut (add_PP (cons k C) (cons (1 + - k) D) = add_PP (cons k0 A) (cons (1 + - k0) B)); intros. elim (classic (k = 0)); intros. left; try assumption. unfold alignes, alignes1 in |- *. right; try assumption. rewrite H0 in H. exists k0. VReplace (cons 1 D) (cons (1 + -0) D). RingPP2 H; RingPP. right; try assumption. exists (/ k * k0). exists (/ k * (1 + - k0)). apply mult_PP_regulier with k; auto. VReplace (mult_PP k (cons 1 C)) (cons k C). RingPP1 H. FieldPP k. rewrite <- H2; trivial. Qed.