proposition: Lemma paralleles_coplanaires : forall A B C D : PO, A <> B -> C <> D -> paralleles (droite A B) (droite C D) -> coplanaires A B C D.
proof: Proof. unfold coplanaires in |- *; intros A B C D H H10 H0. elim def_paralleles2 with (3 := H0); auto. intros k H1. elim (classic (k = 0)); intros. rewrite H2 in H1. absurd (A = B); auto. apply conversion_PP with (a := 1) (b := 1); auto with *. RingPP1 H1. RingPP. right; try assumption. exists (- / k). exists (/ k). apply mult_PP_regulier with k; auto. replace (mult_PP k (add_PP (cons (- / k) A) (add_PP (cons (/ k) B) (cons (1 + - (- / k + / k)) C)))) with (add_PP (cons (-1) A) (add_PP (cons 1 B) (cons k C))). RingPP1 H1. RingPP. FieldPP k. Qed.