proposition: Lemma homothetie_analytique : forall (k : R) (J M M' : PO), M' = homothetie k J M :>PO -> abscisse M' + - abscisse J = k * (abscisse M + - abscisse J) /\ ordonnee M' + - ordonnee J = k * (ordonnee M + - ordonnee J).
proof: Proof. intros. paffixe M z. paffixe J j. paffixe M' z'. assert (Cplus z' (Copp j) = Cmult (Rinj k) (Cplus z (Copp j))). apply rec_complexe_homothetie with (4 := H); auto. generalize H0 H1 H2. repeat rewrite <- coordonnees_affixe; intros. apply unicite_parties_relles_imaginaires with (Cplus z' (Copp j)); auto. rewrite H6; rewrite H5. rewrite Copp_algebrique; rewrite Cplus_algebrique; auto. rewrite H3; rewrite H4; rewrite H5. rewrite Copp_algebrique; rewrite Cplus_algebrique. unfold Rinj in |- *; rewrite Cmult_algebrique. RReplace (k * (abscisse M + - abscisse J) + - (0 * (ordonnee M + - ordonnee J))) (k * (abscisse M + - abscisse J)). RReplace (0 * (abscisse M + - abscisse J) + k * (ordonnee M + - ordonnee J)) (k * (ordonnee M + - ordonnee J)). auto. Qed.