proposition: Theorem rotation_centre_origine_complexe : forall (a : R) (z z' : C) (M M' : PO), z = affixe M -> z' = affixe M' -> M' = rotation O a M -> z' = Cmult (cons_pol 1 a) z.
proof: Proof. intros a z z' M M'; try assumption. discrimine M O. intros. rewrite H1; rewrite H2; rewrite <- rotation_def_centre; rewrite H0; rewrite <- affixe_origine; ring. intros. cut (O <> M); intros. elim rotation_def with (I := O) (A := M) (B := M') (a := a); [ intros | auto | auto ]. cut (O <> M'); intros. cut (z <> zeroC); intros. cut (z' <> zeroC); intros. cut (module z' = module z); intros. apply egalite_forme_polaire; auto with geo. rewrite H9; rewrite Cmult_module; rewrite module_un_trivial; ring. rewrite Cmult_argument; auto with geo. rewrite argument_module_un; rewrite H5. rewrite (angle_argument (z:=z) (z':=z') (M:=M) (M':=M')); auto with geo. elim existence_argument with (z := z); [ intros; try clear existence_argument | auto ]. elim existence_argument with (z := z'); [ intros; try clear existence_argument | auto ]. rewrite H10; rewrite <- mes_opp. rewrite H11; repeat rewrite <- add_mes_compatible. replace (x0 + - x + x) with x0; [ auto | ring ]. rewrite (module_def2 (z:=z) (M:=M)); auto. rewrite (module_def2 (z:=z') (M:=M')); auto. eauto with geo. eauto with geo. apply isometrie_distinct with (1 := H3); auto. auto. Qed.