proposition: Lemma paralleles_vecteur : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> paralleles (droite A B) (droite C D) -> exists k : R, vec A B = mult_PP k (vec C D) :>PP.
proof: Proof. unfold vec in |- *; intros. elim def_paralleles2 with (3 := H1); auto. intros k H2; try assumption. exists k. RingPP1 H2; RingPP. Qed.