proposition: Theorem complexe_rotation_centre_origine : forall (a : R) (z z' : C) (M M' : PO), z = affixe M -> z' = affixe M' -> z' = Cmult (cons_pol 1 a) z -> M' = rotation O a M.
proof: Proof. intros. cut (module z' = module z); intros. discrimine O M. cut (z = zeroC); intros. replace M with M'. rewrite <- rotation_def_centre; auto. apply (egalite_affixe_point (z:=z') (z':=z) (M:=M') (M':=M)); auto. rewrite H1; rewrite H4; ring. apply (egalite_point_image (z:=z) (z':=zeroC) (M:=M) (M':=O)); auto with geo. apply rotation_def2; auto. rewrite <- (module_def2 (z:=z) (M:=M)); auto. rewrite <- (module_def2 (z:=z') (M:=M')); auto. cut (z <> zeroC); intros; [ idtac | eauto with geo ]. cut (z' <> zeroC); intros. cut (O <> M'); intros; [ idtac | eauto with geo ]. rewrite (angle_argument (z:=z) (z':=z') (M:=M) (M':=M')); auto with geo. rewrite H1; rewrite Cmult_argument; auto with geo. rewrite argument_module_un. elim existence_argument with (z := z); [ intros; try clear existence_argument | auto with geo ]. rewrite H7. rewrite <- mes_opp; auto. repeat rewrite <- add_mes_compatible. replace (a + x + - x) with a; [ auto | ring ]. apply nonzero_module. rewrite H2; auto with geo. rewrite H1; rewrite Cmult_module; rewrite module_un_trivial; ring. Qed.