proposition: Lemma existence_homothetique : forall (k : R) (I A : PO), exists A' : PO, A' = homothetie k I A.
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := I) (B := I) (C := A) (k := k); intros A' H1; try clear existence_representant_mult_vecteur. exists A'. apply vecteur_homothetie; auto. Qed.