proposition: Lemma homothetie_droite : forall (k : R) (I A A' B B' : PO), k <> 0 :>R -> A <> B -> A' = homothetie k I A :>PO -> B' = homothetie k I B :>PO -> paralleles (droite A' B') (droite A B).
proof: Proof. intros. apply colineaires_paralleles with k; auto. apply image_homothetie_distincts with (3 := H1) (4 := H2); auto. apply homothetie_bipoint with (I := I); auto. Qed.