proposition: Theorem complexe_homothetie : forall (k : R) (j z z' : C) (J M M' : PO), z = affixe M -> z' = affixe M' -> j = affixe J -> Cplus z' (Copp j) = Cmult (Rinj k) (Cplus z (Copp j)) -> M' = homothetie k J M :>PO.
proof: Proof. intros. apply vecteur_homothetie. apply produit_reel_affixe_vecteur with (3 := H2); auto with geo. Qed.