proposition: Lemma Thales_PP : forall A B C D : PO, A <> C -> B <> D -> paralleles (droite A C) (droite B D) -> exists k : R, add_PP (cons 1 A) (cons k B) = add_PP (cons 1 C) (cons k D) :>PP.
proof: Proof. intros A B C D H10 H11 H; try assumption. elim def_paralleles2 with (3 := H); auto. intros k H2. exists (- k). RingPP1 H2. RingPP. Qed.