proposition: Lemma colineaires_paralleles : forall (k : R) (A B C D : PO), A <> B :>PO -> C <> D :>PO -> vec A B = mult_PP k (vec C D) -> paralleles (droite A B) (droite C D).
proof: Proof. unfold vec in |- *; intros. apply def_paralleles with k; auto. RingPP1 H1; RingPP. Qed.