proposition: Lemma reciproque_Thales_PP : forall (A B C D : PO) (k : R), A <> C :>PO -> B <> D :>PO -> add_PP (cons 1 A) (cons k B) = add_PP (cons 1 C) (cons k D) -> paralleles (droite A C) (droite B D).
proof: Proof. intros A B C D k H10 H11 H; try assumption. apply def_paralleles with (- k); auto. replace (- - k) with k; try ring. RingPP2 H. RingPP. Qed.