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