proposition: Theorem complexe_rotation : forall (a : R) (j z z' : C) (J M M' : PO), z = affixe M -> z' = affixe M' -> j = affixe J -> Cplus z' (Copp j) = Cmult (cons_pol 1 a) (Cplus z (Copp j)) -> M' = rotation J a M.
proof: Proof. intros. cut (module (Cplus z' (Copp j)) = module (Cplus z (Copp j))); intros. discrimine J M. cut (Cplus z (Copp j) = zeroC); intros. replace M with M'. rewrite <- rotation_def_centre; auto. apply egalite_vecteur_point with J. apply (egalite_affixe_vecteur (z:=Cplus z' (Copp j)) (z':= Cplus z (Copp j)) (A:=J) (B:=M') (A':=J) (B':=M)); auto with geo. rewrite H2; rewrite H5; ring. apply (egalite_point_zeroC (z:=Cplus z (Copp j)) (A:=J) (B:=M)); auto with geo. apply rotation_def2; auto. rewrite <- (module_difference (a:=j) (b:=z) (A:=J) (B:=M)); auto. rewrite <- (module_difference (a:=j) (b:=z') (A:=J) (B:=M')); auto. cut (Cplus z (Copp j) <> zeroC); intros; [ idtac | eauto with geo ]. cut (Cplus z' (Copp j) <> zeroC); intros. cut (J <> M'); intros. rewrite (angle_vecteurs_arguments (A:=J) (B:=M) (A':=J) (B':=M') (z:=Cplus z (Copp j)) (z':=Cplus z' (Copp j))); auto with geo. rewrite H2; rewrite Cmult_argument; auto with geo. rewrite argument_module_un. elim existence_argument with (z := Cplus z (Copp j)); [ intros; try clear existence_argument | auto ]. rewrite H8; repeat rewrite <- mes_opp. repeat rewrite <- add_mes_compatible. replace (a + x + - x) with a; [ auto | ring ]. eauto with geo. apply nonzero_module. rewrite H3; auto with geo. rewrite H2; rewrite Cmult_module; rewrite module_un_trivial; ring. Qed.