proposition: Theorem rec_complexe_homothetie : forall (k : R) (j z z' : C) (J M M' : PO), z = affixe M -> z' = affixe M' -> j = affixe J -> M' = homothetie k J M :>PO -> Cplus z' (Copp j) = Cmult (Rinj k) (Cplus z (Copp j)).
proof: Proof. intros. cut (vec J M' = mult_PP k (vec J M)); intros. 2: apply homothetie_vecteur; auto. apply produit_vecteur_image with (3 := H3); auto with geo. Qed.