proposition: Theorem reciproque_Thales_expl : forall (A B C D I : PO) (k : R), A <> C :>PO -> B <> D :>PO -> vec I A = mult_PP k (vec I B) :>PP -> vec I C = mult_PP k (vec I D) :>PP -> paralleles (droite A C) (droite B D).
proof: Proof. unfold vec in |- *; intros A B C D I k H10 H11 H H0. apply reciproque_Thales_PP with (- k); auto. RingPP2 H. RingPP2 H0. RingPP. Qed.