proposition: Theorem paralleles_homothetie : forall A B C I J : PO, triangle A B C -> I <> J :>PO -> alignes A B I -> paralleles (droite B C) (droite I J) -> alignes A C J -> exists k : R, I = homothetie k A B :>PO /\ J = homothetie k A C :>PO.
proof: Proof. intros. deroule_triangle A B C. halignes H1 x. cut (triangle B C A); intros; auto with geo. elim (classic (x = 0)); intros. cut (A = I); intros. absurd (paralleles (droite I J) (droite B C)); auto with geo. rewrite (droite_permute (A:=I) (B:=J)); auto. apply concours_non_paralleles; auto. rewrite <- H11; auto. apply def_concours with C; auto with geo. rewrite <- H11; auto. apply alignes_ordre_cycle; auto with geo. apply vecteur_nul_conf. rewrite H8; rewrite H10; Ringvec. exists x; split; apply vecteur_homothetie; auto. generalize (Thales_concours (k:=x) (A:=A) (B:=B) (C:=C) (I:=I)); intros H18; apply H18; auto. Qed.