fact: Axiom def_paralleles2 : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> paralleles (droite A B) (droite C D) -> exists k : R, add_PP (cons 1 B) (cons (-1) A) = add_PP (cons k D) (cons (- k) C) :>PP.