proposition: Lemma similitude_analytique : forall (k a : R) (J M M' : PO), k > 0 -> M' = similitude J k a M -> abscisse M' + - abscisse J = k * (cos a * (abscisse M + - abscisse J) + - (sin a * (ordonnee M + - ordonnee J))) /\ ordonnee M' + - ordonnee J = k * (sin a * (abscisse M + - abscisse J) + cos a * (ordonnee M + - ordonnee J)).
proof: Proof. intros. assert (k <> 0); auto with real. assert (cons_pol k a = cons_cart (k * cos a) (k * sin a)). elim existence_parties_relles_imaginaires with (z := cons_pol k a); [ intros a0 H2; elim H2; [ intros b H3 ] ]. assert (a0 = k * cos a /\ b = k * sin a). apply passage_polaire_algebrique with (cons_pol k a); auto with geo. elim H4; [ intros H5 H6; try clear H4; try exact H6 ]. rewrite H3; rewrite H5; rewrite H6. auto. paffixe M z. paffixe J j. paffixe M' z'. assert (Cplus z' (Copp j) = Cmult (cons_pol k a) (Cplus z (Copp j))). apply similitude_complexe with (5 := H0); auto. generalize H3 H4 H5. repeat rewrite <- coordonnees_affixe; intros. apply unicite_parties_relles_imaginaires with (Cplus z' (Copp j)); auto. rewrite H9; rewrite H8. rewrite Copp_algebrique; rewrite Cplus_algebrique; auto. rewrite H6; rewrite H7; rewrite H8. rewrite Copp_algebrique; rewrite Cplus_algebrique. rewrite H2; rewrite Cmult_algebrique. RReplace (k * cos a * (abscisse M + - abscisse J) + - (k * sin a * (ordonnee M + - ordonnee J))) (k * (cos a * (abscisse M + - abscisse J) + - (sin a * (ordonnee M + - ordonnee J)))). RReplace (k * sin a * (abscisse M + - abscisse J) + k * cos a * (ordonnee M + - ordonnee J)) (k * (sin a * (abscisse M + - abscisse J) + cos a * (ordonnee M + - ordonnee J))). auto. Qed.